-- The plane: closed rectangles are compact in the product topology of two
-- copies of the line
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Topology.Plane
import Tube
import HeineBorel

def planeTopology : Set := productTopology(ℝ, realTopology, ℝ, realTopology)

theorem planeTopology.topology
  shows IsTopology(ℝ × ℝ, planeTopology)
proof
  unfold planeTopology
  exact productTopology.topology with realTopology.topology, realTopology.topology

theorem closedRectangle.compact (A B C D : Real)
  requires orderedX : A ≤ B
  requires orderedY : C ≤ D
  shows IsCompact(ℝ × ℝ, planeTopology, closedInterval(A, B) × closedInterval(C, D))
proof
  have compactX := closedInterval.compact with orderedX
  have compactY := closedInterval.compact with orderedY
  unfold planeTopology
  exact IsCompact.product with realTopology.topology, realTopology.topology, compactX, compactY