Grace/Cumulus/Topology/Basis.g17

Open in Workbench Download source

Imports

Separation · Real

Declarations

Source

1-- Bases of a topology: every open set is a union of basis sets, the2-- topology generated by a family satisfying the basis axioms, closure,3-- interior, and continuity tested on a basis, bases of subspaces and4-- products, and the open balls as a basis of the real line5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Topology.Basis11import Separation12import Real1314predicate Basis (X T B : Set) :=15  B ⊆ T ∧ (∀ U ∈ T, ∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U)1617theorem Basis.subset (X T B : Set)18  requires basis : Basis(X, T, B)19  shows B ⊆ T20proof21  exact basis.left2223theorem Basis.refine (X T B U x : Set)24  requires basis : Basis(X, T, B)25  requires hU : U ∈ T26  requires hx : x ∈ U27  shows ∃ W ∈ B, x ∈ W ∧ W ⊆ U28proof29  exact basis.right with U, hU, x, hx3031theorem Basis.self (X T : Set)32  shows Basis(X, T, T)33proof34  constructor35  . exact Subset.reflexive at T36  . intros U hU x hx37    exact ⟨U, hU, hx, (Subset.reflexive at U)⟩3839-- The basis sets inside U.4041def basisBelow (B U : Set) : Set := { W ∈ B | W ⊆ U }4243theorem basisBelow.union (B U : Set)44  requires refines : ∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U45  shows U = ⋃(basisBelow(B, U))46proof47  apply Subset.antisymmetric48  . intros x hx49    obtain ⟨W, hW, hxW, below⟩ := refines with x, hx50    have found : W ∈ basisBelow(B, U) := basisBelow.membership.backward with ⟨hW, below⟩51    exact union.contains with found, hxW52  . apply union.subset53    intros W hW54    have parts := basisBelow.membership.forward with hW55    exact parts.right5657theorem basisBelow.open (X T B U : Set)58  requires topology : IsTopology(X, T)59  requires inside : B ⊆ T60  shows ⋃(basisBelow(B, U)) ∈ T61proof62  apply IsTopology.union with topology63  intros W hW64  have parts := basisBelow.membership.forward with hW65  exact inside with W, parts.left6667-- Every open set is the union of the basis sets inside it.68theorem Basis.open_union (X T B U : Set)69  requires basis : Basis(X, T, B)70  requires hU : U ∈ T71  shows U = ⋃(basisBelow(B, U))72proof73  apply basisBelow.union74  intros x hx75  exact basis.right with U, hU, x, hx7677theorem Basis.open_iff (X T B U : Set)78  requires topology : IsTopology(X, T)79  requires basis : Basis(X, T, B)80  shows U ∈ T ↔ U ⊆ X ∧ (∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U)81proof82  constructor83  . intro hU84    constructor85    . exact IsTopology.subset with topology, hU86    . intros x hx87      exact basis.right with U, hU, x, hx88  . intro h89    obtain ⟨inside, refines⟩ := h90    have equal := basisBelow.union with refines91    rw equal92    exact basisBelow.open with topology, basis.left9394theorem Basis.covers (X T B : Set)95  requires topology : IsTopology(X, T)96  requires basis : Basis(X, T, B)97  shows ⋃(B) = X98proof99  apply Subset.antisymmetric100  . apply union.subset101    intros W hW102    exact IsTopology.subset with topology, (basis.left with W, hW)103  . intros x hx104    obtain ⟨W, hW, hxW, inside⟩ := basis.right with X, (IsTopology.whole with topology), x, hx105    exact union.contains with hW, hxW106107theorem Basis.meet (X T B W1 W2 x : Set)108  requires topology : IsTopology(X, T)109  requires basis : Basis(X, T, B)110  requires hW1 : W1 ∈ B111  requires hW2 : W2 ∈ B112  requires hx : x ∈ W1 ∩ W2113  shows ∃ W ∈ B, x ∈ W ∧ W ⊆ W1 ∩ W2114proof115  have openMeet := IsTopology.intersection2 with topology, (basis.left with W1, hW1), (basis.left with W2, hW2)116  exact basis.right with W1 ∩ W2, openMeet, x, hx117118-- The basis axioms: a family of subsets of X that covers X and refines119-- pairwise intersections; such a family generates a topology.120121predicate BasisAxioms (X B : Set) :=122  B ⊆ 𝒫(X) ∧ (∀ x ∈ X, ∃ W ∈ B, x ∈ W) ∧123  (∀ W1 ∈ B, ∀ W2 ∈ B, ∀ x ∈ W1 ∩ W2, ∃ W ∈ B, x ∈ W ∧ W ⊆ W1 ∩ W2)124125theorem Basis.axioms (X T B : Set)126  requires topology : IsTopology(X, T)127  requires basis : Basis(X, T, B)128  shows BasisAxioms(X, B)129proof130  refine ⟨?_, ?_, ?_⟩131  . intros W hW132    apply powerset.membership_iff.backward133    exact IsTopology.subset with topology, (basis.left with W, hW)134  . intros x hx135    obtain ⟨W, hW, hxW, inside⟩ := basis.right with X, (IsTopology.whole with topology), x, hx136    exact ⟨W, hW, hxW⟩137  . intros W1 hW1 W2 hW2 x hx138    exact Basis.meet with topology, basis, hW1, hW2, hx139140def generatedTopology (X B : Set) : Set :=141  { U ∈ 𝒫(X) | ∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U }142143theorem generatedTopology.contains (X B : Set)144  requires axioms : BasisAxioms(X, B)145  shows B ⊆ generatedTopology(X, B)146proof147  intros W hW148  apply generatedTopology.membership.backward149  refine ⟨(axioms.left with W, hW), ?_⟩150  intros x hx151  exact ⟨W, hW, hx, (Subset.reflexive at W)⟩152153theorem generatedTopology.topology (X B : Set)154  requires axioms : BasisAxioms(X, B)155  shows IsTopology(X, generatedTopology(X, B))156proof157  obtain ⟨inside, covers, meets⟩ := axioms158  refine ⟨?_, ?_, ?_, ?_⟩159  . intros U hU160    have parts := generatedTopology.membership.forward with hU161    exact parts.left162  . apply generatedTopology.membership.backward163    refine ⟨(powerset.self at X), ?_⟩164    intros x hx165    obtain ⟨W, hW, hxW⟩ := covers with x, hx166    have below := powerset.membership_iff.forward with (inside with W, hW)167    exact ⟨W, hW, hxW, below⟩168  . intros S hS169    apply generatedTopology.membership.backward170    constructor171    . apply powerset.membership_iff.backward172      apply union.subset173      intros U hU174      have parts := generatedTopology.membership.forward with (hS with U, hU)175      exact powerset.membership_iff.forward with parts.left176    . intros x hx177      obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx178      have parts := generatedTopology.membership.forward with (hS with U, hU)179      obtain ⟨W, hW, hxW, below⟩ := parts.right with x, hxU180      refine ⟨W, hW, hxW, ?_⟩181      exact Subset.transitive with below, (union.subset_of_member with hU)182  . intros U hU V hV183    have partsU := generatedTopology.membership.forward with hU184    have partsV := generatedTopology.membership.forward with hV185    apply generatedTopology.membership.backward186    constructor187    . apply powerset.membership_iff.backward188      have insideU := powerset.membership_iff.forward with partsU.left189      exact Subset.transitive with (intersection.subset_left at U, V), insideU190    . intros x hx191      have both := intersection.membership.forward with hx192      obtain ⟨W1, hW1, hxW1, belowU⟩ := partsU.right with x, both.left193      obtain ⟨W2, hW2, hxW2, belowV⟩ := partsV.right with x, both.right194      have inMeet : x ∈ W1 ∩ W2 := intersection.membership.backward with ⟨hxW1, hxW2⟩195      obtain ⟨W, hW, hxW, below⟩ := meets with W1, hW1, W2, hW2, x, inMeet196      refine ⟨W, hW, hxW, ?_⟩197      exact Subset.transitive with below, (intersection.monotone with belowU, belowV)198199theorem generatedTopology.basis (X B : Set)200  requires axioms : BasisAxioms(X, B)201  shows Basis(X, generatedTopology(X, B), B)202proof203  constructor204  . exact generatedTopology.contains with axioms205  . intros U hU x hx206    have parts := generatedTopology.membership.forward with hU207    exact parts.right with x, hx208209-- The generated topology is the coarsest topology containing B.210theorem generatedTopology.coarsest (X T B : Set)211  requires topology : IsTopology(X, T)212  requires inside : B ⊆ T213  shows generatedTopology(X, B) ⊆ T214proof215  intros U hU216  have parts := generatedTopology.membership.forward with hU217  have equal := basisBelow.union with parts.right218  rw equal219  exact basisBelow.open with topology, inside220221theorem Basis.generated (X T B : Set)222  requires topology : IsTopology(X, T)223  requires basis : Basis(X, T, B)224  shows T = generatedTopology(X, B)225proof226  apply Subset.antisymmetric227  . intros U hU228    apply generatedTopology.membership.backward229    constructor230    . exact powerset.membership_iff.backward with (IsTopology.subset with topology, hU)231    . intros x hx232      exact basis.right with U, hU, x, hx233  . exact generatedTopology.coarsest with topology, basis.left234235-- Two bases of the same space determine each other's topology.236theorem Basis.unique_topology (X T T2 B : Set)237  requires topology : IsTopology(X, T)238  requires topology2 : IsTopology(X, T2)239  requires basis : Basis(X, T, B)240  requires basis2 : Basis(X, T2, B)241  shows T = T2242proof243  have first := Basis.generated with topology, basis244  have second := Basis.generated with topology2, basis2245  rw [first, second]246  rfl247248-- Closure, interior, and continuity are tested on a basis.249250theorem Basis.closure_membership (X T B A x : Set)251  requires topology : IsTopology(X, T)252  requires basis : Basis(X, T, B)253  requires hA : A ⊆ X254  shows x ∈ closure(X, T, A) ↔ x ∈ X ∧ (∀ W ∈ B, x ∈ W → Nonempty(W ∩ A))255proof256  have characterization := closure.membership at X, T, A, x with topology, hA257  constructor258  . intro hx259    have parts := characterization.forward with hx260    refine ⟨parts.left, ?_⟩261    intros W hW hxW262    exact parts.right with W, (basis.left with W, hW), hxW263  . intro h264    obtain ⟨hxX, meets⟩ := h265    apply characterization.backward266    refine ⟨hxX, ?_⟩267    intros U hU hxU268    obtain ⟨W, hW, hxW, below⟩ := basis.right with U, hU, x, hxU269    obtain ⟨a, ha⟩ := meets with W, hW, hxW270    have inner := intersection.membership.forward with ha271    witness a272    exact intersection.membership.backward with ⟨(below with a, inner.left), inner.right⟩273274theorem Basis.interior_membership (X T B A x : Set)275  requires basis : Basis(X, T, B)276  shows x ∈ interiorIn(T, A) ↔ ∃ W ∈ B, x ∈ W ∧ W ⊆ A277proof278  have characterization := interiorIn.membership at T, A, x279  constructor280  . intro hx281    obtain ⟨U, hU, hxU, below⟩ := characterization.forward with hx282    obtain ⟨W, hW, hxW, belowU⟩ := basis.right with U, hU, x, hxU283    exact ⟨W, hW, hxW, (Subset.transitive with belowU, below)⟩284  . intro h285    obtain ⟨W, hW, hxW, below⟩ := h286    apply characterization.backward287    exact ⟨W, (basis.left with W, hW), hxW, below⟩288289theorem ContinuousMap.of_basis (f X T Y S B : Set)290  requires topology : IsTopology(X, T)291  requires basis : Basis(Y, S, B)292  requires function : f : X → Y293  requires pulledOpen : ∀ W ∈ B, functionPreimage(f, X, W) ∈ T294  shows ContinuousMap(f, X, T, Y, S)295proof296  constructor297  . exact function298  . intros V hV299    have equal : functionPreimage(f, X, V) = ⋃(preimages(f, X, basisBelow(B, V)))300      ext x301      constructor302      . intro hx303        have parts := functionPreimage.membership.forward with hx304        obtain ⟨W, hW, inW, below⟩ := basis.right with V, hV, f(x), parts.right305        have found : W ∈ basisBelow(B, V) := basisBelow.membership.backward with ⟨hW, below⟩306        have pulled : functionPreimage(f, X, W) ∈ preimages(f, X, basisBelow(B, V)) := preimages.membership.backward with ⟨W, found, rfl⟩307        have inPreimage : x ∈ functionPreimage(f, X, W) := functionPreimage.membership.backward with ⟨parts.left, inW⟩308        exact union.contains with pulled, inPreimage309      . intro hx310        obtain ⟨P, hP, hxP⟩ := union.membership.forward with hx311        obtain ⟨W, hW, shape⟩ := preimages.membership.forward with hP312        rw ← shape at hxP313        have parts := functionPreimage.membership.forward with hxP314        have belowParts := basisBelow.membership.forward with hW315        apply functionPreimage.membership.backward316        exact ⟨parts.left, (belowParts.right with f(x), parts.right)⟩317    rw equal318    apply IsTopology.union with topology319    intros P hP320    obtain ⟨W, hW, shape⟩ := preimages.membership.forward with hP321    rw ← shape322    have belowParts := basisBelow.membership.forward with hW323    exact pulledOpen with W, belowParts.left324325-- Bases of subspaces and products.326327theorem Basis.subspace (X T B A : Set)328  requires basis : Basis(X, T, B)329  requires hA : A ⊆ X330  shows Basis(A, subspaceTopology(T, A), subspaceTopology(B, A))331proof332  constructor333  . intros W hW334    obtain ⟨W0, hW0, shape⟩ := subspaceTopology.membership.forward with hW335    apply subspaceTopology.membership.backward336    exact ⟨W0, (basis.left with W0, hW0), shape⟩337  . intros V hV x hx338    obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with hV339    rw ← shape at hx340    have parts := intersection.membership.forward with hx341    obtain ⟨W, hW, hxW, below⟩ := basis.right with U, hU, x, parts.left342    have traced : W ∩ A ∈ subspaceTopology(B, A) := subspaceTopology.membership.backward with ⟨W, hW, rfl⟩343    refine ⟨W ∩ A, traced, (intersection.membership.backward with ⟨hxW, parts.right⟩), ?_⟩344    rw ← shape345    exact intersection.monotone_left with below346347def boxes (X T Y S : Set) : Set :=348  { W ∈ 𝒫(X × Y) | ∃ U ∈ T, ∃ V ∈ S, W = U × V }349350theorem Basis.product (X T Y S : Set)351  requires topologyX : IsTopology(X, T)352  requires topologyY : IsTopology(Y, S)353  shows Basis(X × Y, productTopology(X, T, Y, S), boxes(X, T, Y, S))354proof355  constructor356  . intros W hW357    have parts := boxes.membership.forward with hW358    obtain ⟨U, hU, V, hV, shape⟩ := parts.right359    rw shape360    exact productTopology.box with topologyX, topologyY, hU, hV361  . intros W hW p hp362    have parts := productTopology.membership.forward with hW363    obtain ⟨U, hU, V, hV, inBox, below⟩ := parts.right with p, hp364    have inside := product.monotone with (IsTopology.subset with topologyX, hU), (IsTopology.subset with topologyY, hV)365    have found : U × V ∈ boxes(X, T, Y, S)366      apply boxes.membership.backward367      exact ⟨(powerset.membership_iff.backward with inside), U, hU, V, hV, rfl⟩368    exact ⟨U × V, found, inBox, below⟩369370-- The open balls form a basis of the real line.371372def openBalls : Set :=373  { W ∈ 𝒫(ℝ) | ∃ C ∈ ℝ, ∃ E ∈ ℝ, 0 < E ∧ W = openBall(C, E) }374375theorem openBall.member_balls (C E : Real)376  requires positive : 0 < E377  shows openBall(C, E) ∈ openBalls378proof379  have realC : C ∈ ℝ by typecheck380  have realE : E ∈ ℝ by typecheck381  apply openBalls.membership.backward382  exact ⟨(powerset.membership_iff.backward with (openBall.subset_reals at C, E)), C, realC, E, realE, positive, rfl⟩383384theorem realTopology.basis385  shows Basis(ℝ, realTopology, openBalls)386proof387  constructor388  . intros W hW389    have parts := openBalls.membership.forward with hW390    obtain ⟨C, hC, E, hE, positive, shape⟩ := parts.right391    rw shape392    exact openBall.open at C, E393  . intros U hU x hx394    have parts := realTopology.membership.forward with hU395    have inside := powerset.membership_iff.forward with parts.left396    have hxR := inside with x, hx397    obtain ⟨E, hE, positive, below⟩ := parts.right with x, hx398    have center := openBall.center at x, E with positive399    have found := openBall.member_balls at x, E with positive400    exact ⟨openBall(x, E), found, center, below⟩401