Grace/Cumulus/Topology/Plane.g17

Open in Workbench Download source

Imports

Tube · HeineBorel

Declarations

• planeTopology def
• planeTopology.topology theorem derivation
• closedRectangle.compact theorem derivation

Source

1-- The plane: closed rectangles are compact in the product topology of two2-- copies of the line3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Topology.Plane9import Tube10import HeineBorel1112def planeTopology : Set := productTopology(ℝ, realTopology, ℝ, realTopology)1314theorem planeTopology.topology15  shows IsTopology(ℝ × ℝ, planeTopology)16proof17  unfold planeTopology18  exact productTopology.topology with realTopology.topology, realTopology.topology1920theorem closedRectangle.compact (A B C D : Real)21  requires orderedX : A ≤ B22  requires orderedY : C ≤ D23  shows IsCompact(ℝ × ℝ, planeTopology, closedInterval(A, B) × closedInterval(C, D))24proof25  have compactX := closedInterval.compact with orderedX26  have compactY := closedInterval.compact with orderedY27  unfold planeTopology28  exact IsCompact.product with realTopology.topology, realTopology.topology, compactX, compactY29