Grace/Cumulus/Topology/Compact.g17

Open in Workbench Download source

Imports

Continuity · Cardinal.FiniteImage

Declarations

Source

1-- Compactness: every open cover has a finite subcover. Finite sets are2-- compact, compactness passes to finite unions and to closed subsets; the3-- preimages of a cover along a map4-- 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.Compact10import Continuity11import Cardinal.FiniteImage1213predicate OpenCover (T A C : Set) := (C ⊆ T) ∧ (A ⊆ ⋃(C))14predicate IsCompact (X T A : Set) :=15  (A ⊆ X) ∧ (∀ C, OpenCover(T, A, C) → ∃ F, F ⊆ C ∧ Finite(F) ∧ A ⊆ ⋃(F))1617theorem IsCompact.subset (X T A : Set)18  requires compact : IsCompact(X, T, A)19  shows A ⊆ X20proof21  exact compact.left2223theorem IsCompact.subcover (X T A C : Set)24  requires compact : IsCompact(X, T, A)25  requires cover : OpenCover(T, A, C)26  shows ∃ F, F ⊆ C ∧ Finite(F) ∧ A ⊆ ⋃(F)27proof28  exact compact.right with C, cover2930theorem IsCompact.empty (X T : Set)31  shows IsCompact(X, T, ∅)32proof33  constructor34  . exact empty.subset at X35  . intros C cover36    witness ∅37    refine ⟨(empty.subset at C), Finite.empty, (empty.subset at ⋃(∅))⟩3839theorem IsCompact.singleton (X T x : Set)40  requires hx : x ∈ X41  shows IsCompact(X, T, {x})42proof43  constructor44  . intros y hy45    have same := singleton.membership.forward with hy46    rwa same47  . intros C cover48    have self : x ∈ {x} by simp [singleton.membership]49    have covered := cover.right with x, self50    obtain ⟨U, hU, hxU⟩ := union.membership.forward with covered51    witness {U}52    refine ⟨?_, (Finite.singleton at U), ?_⟩53    . intros V hV54      have same := singleton.membership.forward with hV55      rwa same56    . intros y hy57      have same := singleton.membership.forward with hy58      rwa [same, union.singleton]5960theorem IsCompact.union2 (X T A B : Set)61  requires compactA : IsCompact(X, T, A)62  requires compactB : IsCompact(X, T, B)63  shows IsCompact(X, T, A ∪ B)64proof65  constructor66  . exact union2.subset with compactA.left, compactB.left67  . intros C cover68    have coverA : OpenCover(T, A, C)69      constructor70      . exact cover.left71      . exact Subset.transitive with (union2.subset_left at A, B), cover.right72    have coverB : OpenCover(T, B, C)73      constructor74      . exact cover.left75      . exact Subset.transitive with (union2.subset_right at A, B), cover.right76    obtain ⟨F, hF, finiteF, coveredA⟩ := compactA.right with C, coverA77    obtain ⟨G, hG, finiteG, coveredB⟩ := compactB.right with C, coverB78    witness F ∪ G79    refine ⟨(union2.subset with hF, hG), (Finite.union with finiteF, finiteG), ?_⟩80    rw union.union281    exact union2.monotone with coveredA, coveredB8283-- A closed subset of a compact set is compact: add the complement to a84-- cover of the subset, take a finite subcover of the whole, drop it again.85theorem IsCompact.closed_subset (X T A C : Set)86  requires topology : IsTopology(X, T)87  requires compact : IsCompact(X, T, A)88  requires closed : IsClosed(X, T, C)89  requires hCA : C ⊆ A90  shows IsCompact(X, T, C)91proof92  have hCX := closed.left93  constructor94  . exact hCX95  . intros D cover96    have extendedOpen : insert(complement(X, C), D) ⊆ T97      intros U hU98      have split := insert.membership.forward with hU99      cases split with isComplement | inD100      . rw isComplement101        exact closed.right102      . exact cover.left with U, inD103    have extendedCover : A ⊆ ⋃(insert(complement(X, C), D))104      intros a ha105      have haX := compact.left with a, ha106      have split : a ∈ C ∨ ¬a ∈ C by tauto107      cases split with inC | outside108      . have covered := cover.right with a, inC109        obtain ⟨U, hU, haU⟩ := union.membership.forward with covered110        have member : U ∈ insert(complement(X, C), D)111          apply insert.membership.backward112          right113          exact hU114        exact union.contains with member, haU115      . have inComplement : a ∈ complement(X, C) := complement.membership.backward with ⟨haX, outside⟩116        have member : complement(X, C) ∈ insert(complement(X, C), D)117          apply insert.membership.backward118          left119          rfl120        exact union.contains with member, inComplement121    obtain ⟨F, hF, finiteF, coveredA⟩ := compact.right with insert(complement(X, C), D), ⟨extendedOpen, extendedCover⟩122    witness F ∖ {complement(X, C)}123    refine ⟨?_, (Finite.subset with finiteF, (difference.subset_left at F, {complement(X, C)})), ?_⟩124    . intros U hU125      have parts := difference.singleton_membership.forward with hU126      have split := insert.membership.forward with (hF with U, parts.left)127      cases split with isComplement | inD128      . exfalso129        exact parts.right with isComplement130      . exact inD131    . intros c hc132      have covered := coveredA with c, (hCA with c, hc)133      obtain ⟨U, hU, hcU⟩ := union.membership.forward with covered134      have kept : U ∈ F ∖ {complement(X, C)}135        apply difference.singleton_membership.backward136        refine ⟨hU, ?_⟩137        intro isComplement138        rw isComplement at hcU139        have away := complement.membership.forward with hcU140        exact away.right with hc141      exact union.contains with kept, hcU142143-- The preimages of the members of a family C along f, and the members of144-- C whose preimage is a given set.145def preimages (f X C : Set) : Set := { functionPreimage(f, X, V) | V ∈ C }146def originals (f X C U : Set) : Set := { V ∈ C | functionPreimage(f, X, V) = U }147