Grace/Cumulus/Topology/Product.g17

Open in Workbench Download source

Imports

Subspace

Declarations

• productTopology def
• productTopology.box theorem derivation
• productTopology.topology theorem derivation
• firstProjection.continuous theorem derivation
• secondProjection.continuous theorem derivation

Source

1-- The product of two topological spaces: a set is open when every point2-- has an open box inside it. The coordinate projections are continuous,3-- and open boxes are open4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Topology.Product10import Subspace1112-- The product topology.13def productTopology (X T Y S : Set) : Set :=14  { W ∈ 𝒫(X × Y) | ∀ p ∈ W, ∃ U ∈ T, ∃ V ∈ S, p ∈ U × V ∧ U × V ⊆ W }1516theorem productTopology.box (X T Y S U V : Set)17  requires topologyX : IsTopology(X, T)18  requires topologyY : IsTopology(Y, S)19  requires hU : U ∈ T20  requires hV : V ∈ S21  shows U × V ∈ productTopology(X, T, Y, S)22proof23  apply productTopology.membership.backward24  have inside := product.monotone with (IsTopology.subset with topologyX, hU), (IsTopology.subset with topologyY, hV)25  refine ⟨(powerset.membership_iff.backward with inside), ?_⟩26  intros p hp27  refine ⟨U, hU, V, hV, hp, (Subset.reflexive at U × V)⟩2829theorem productTopology.topology (X T Y S : Set)30  requires topologyX : IsTopology(X, T)31  requires topologyY : IsTopology(Y, S)32  shows IsTopology(X × Y, productTopology(X, T, Y, S))33proof34  constructor35  . intros W hW36    have parts := productTopology.membership.forward with hW37    exact parts.left38  . constructor39    . exact productTopology.box with topologyX, topologyY, (IsTopology.whole with topologyX), (IsTopology.whole with topologyY)40    . constructor41      . intros F hF42        apply productTopology.membership.backward43        constructor44        . apply powerset.membership_iff.backward45          apply union.subset46          intros W hW47          have parts := productTopology.membership.forward with (hF with W, hW)48          exact powerset.membership_iff.forward with parts.left49        . intros p hp50          obtain ⟨W, hW, hpW⟩ := union.membership.forward with hp51          have parts := productTopology.membership.forward with (hF with W, hW)52          obtain ⟨U, hU, V, hV, inBox, boxInside⟩ := parts.right with p, hpW53          refine ⟨U, hU, V, hV, inBox, ?_⟩54          exact Subset.transitive with boxInside, (union.subset_of_member with hW)55      . intros W1 hW1 W2 hW256        have parts1 := productTopology.membership.forward with hW157        have parts2 := productTopology.membership.forward with hW258        have inside1 := powerset.membership_iff.forward with parts1.left59        apply productTopology.membership.backward60        constructor61        . apply powerset.membership_iff.backward62          exact Subset.transitive with (intersection.subset_left at W1, W2), inside163        . intros p hp64          have both := intersection.membership.forward with hp65          obtain ⟨U1, hU1, V1, hV1, inBox1, boxInside1⟩ := parts1.right with p, both.left66          obtain ⟨U2, hU2, V2, hV2, inBox2, boxInside2⟩ := parts2.right with p, both.right67          have boxes := product.intersection at U1, U2, V1, V268          refine ⟨U1 ∩ U2, (IsTopology.intersection2 with topologyX, hU1, hU2), V1 ∩ V2, (IsTopology.intersection2 with topologyY, hV1, hV2), ?_, ?_⟩69          . rw boxes70            exact intersection.membership.backward with ⟨inBox1, inBox2⟩71          . rw boxes72            exact intersection.monotone with boxInside1, boxInside27374-- Projections are continuous: the preimage of U is the box U × Y.75theorem firstProjection.continuous (X T Y S : Set)76  requires topologyX : IsTopology(X, T)77  requires topologyY : IsTopology(Y, S)78  shows ContinuousMap(firstProjection(X, Y), X × Y, productTopology(X, T, Y, S), X, T)79proof80  have function := firstProjection.function at X, Y81  constructor82  . exact function83  . intros U hU84    have inside := IsTopology.subset with topologyX, hU85    have same : functionPreimage(firstProjection(X, Y), X × Y, U) = U × Y86      ext p87      constructor88      . intro hp89        have parts := functionPreimage.membership.forward with hp90        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with parts.left91        have value := firstProjection.pair with hx, hy92        rw [shape, value] at parts93        rw shape94        exact product.pair with parts.right, hy95      . intro hp96        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp97        have hxX := inside with x, hx98        have value := firstProjection.pair with hxX, hy99        apply functionPreimage.membership.backward100        rw [shape, value]101        exact ⟨(product.pair with hxX, hy), hx⟩102    rw same103    exact productTopology.box with topologyX, topologyY, hU, (IsTopology.whole with topologyY)104105theorem secondProjection.continuous (X T Y S : Set)106  requires topologyX : IsTopology(X, T)107  requires topologyY : IsTopology(Y, S)108  shows ContinuousMap(secondProjection(X, Y), X × Y, productTopology(X, T, Y, S), Y, S)109proof110  have function := secondProjection.function at X, Y111  constructor112  . exact function113  . intros V hV114    have inside := IsTopology.subset with topologyY, hV115    have same : functionPreimage(secondProjection(X, Y), X × Y, V) = X × V116      ext p117      constructor118      . intro hp119        have parts := functionPreimage.membership.forward with hp120        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with parts.left121        have value := secondProjection.pair with hx, hy122        rw [shape, value] at parts123        rw shape124        exact product.pair with hx, parts.right125      . intro hp126        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp127        have hyY := inside with y, hy128        have value := secondProjection.pair with hx, hyY129        apply functionPreimage.membership.backward130        rw [shape, value]131        exact ⟨(product.pair with hx, hyY), hy⟩132    rw same133    exact productTopology.box with topologyX, topologyY, (IsTopology.whole with topologyX), hV134