Grace/Cumulus/Topology/CompactMore.g17

Open in Workbench Download source

Imports

Separation · Cardinal.FiniteUnion · Set.Choice

Declarations

Source

1-- More compactness: finite sets and finite unions of compact sets are2-- compact, a compact set meets a closed set in a compact set, compact3-- sets in Hausdorff spaces are closed and separate from points and from4-- each other, a compact Hausdorff space is regular and normal, and a5-- family of closed sets with the finite intersection property meets6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Topology.CompactMore12import Separation13import Cardinal.FiniteUnion14import Set.Choice1516-- Finite sets are compact: pick one cover member through each point.1718def coverMembers (C a : Set) : Set := { U ∈ C | a ∈ U }1920defgraph coverChoice (C A : Set) (a ∈ A) : C := choose(coverMembers(C, a))21requires covers : A ⊆ ⋃(C)22proof23  have covered := covers with a, member24  obtain ⟨U, hU, haU⟩ := union.membership.forward with covered25  have found : U ∈ coverMembers(C, a) := coverMembers.membership.backward with ⟨hU, haU⟩26  have inhabited : Nonempty(coverMembers(C, a)) := ⟨U, found⟩27  have chosen := choose.member with inhabited28  have parts := coverMembers.membership.forward with chosen29  exact parts.left3031theorem coverChoice.selected (C A a : Set)32  requires covers : A ⊆ ⋃(C)33  requires ha : a ∈ A34  shows coverChoice(C, A)(a) ∈ coverMembers(C, a)35proof36  have value := coverChoice.value with covers, ha37  rw value38  have covered := covers with a, ha39  obtain ⟨U, hU, haU⟩ := union.membership.forward with covered40  have found : U ∈ coverMembers(C, a) := coverMembers.membership.backward with ⟨hU, haU⟩41  have inhabited : Nonempty(coverMembers(C, a)) := ⟨U, found⟩42  exact choose.member with inhabited4344theorem IsCompact.finite (X T A : Set)45  requires finite : Finite(A)46  requires hA : A ⊆ X47  shows IsCompact(X, T, A)48proof49  constructor50  . exact hA51  . intros C cover52    have covers := cover.right53    have graph := coverChoice.function with covers54    witness functionImage(coverChoice(C, A), A, C)55    refine ⟨(functionImage.subset at coverChoice(C, A), A, C), (Finite.function_image with graph, finite, (Subset.reflexive at A)), ?_⟩56    intros a ha57    have selected := coverChoice.selected with covers, ha58    have parts := coverMembers.membership.forward with selected59    have imageMember := functionImage.value with graph, ha60    exact union.contains with imageMember, parts.right6162theorem IsCompact.whole_of_finite (X T : Set)63  requires finite : Finite(X)64  shows IsCompact(X, T, X)65proof66  exact IsCompact.finite with finite, (Subset.reflexive at X)6768-- A finite union of compact sets is compact: choose a finite subcover of69-- each member and take their union.7071def finiteSubcovers (C A : Set) : Set := { G ∈ 𝒫(C) | Finite(G) ∧ A ⊆ ⋃(G) }7273defgraph subcoverChoice (X T C F : Set) (A ∈ F) : 𝒫(C) := choose(finiteSubcovers(C, A))74requires compact : ∀ B ∈ F, IsCompact(X, T, B)75requires cover : OpenCover(T, ⋃(F), C)76proof77  have compactA := compact with A, member78  have below := union.subset_of_member with member79  have coverA : OpenCover(T, A, C) := ⟨cover.left, (Subset.transitive with below, cover.right)⟩80  obtain ⟨G, hG, finiteG, covered⟩ := compactA.right with C, coverA81  have found : G ∈ finiteSubcovers(C, A) := finiteSubcovers.membership.backward with ⟨(powerset.membership_iff.backward with hG), finiteG, covered⟩82  have inhabited : Nonempty(finiteSubcovers(C, A)) := ⟨G, found⟩83  have chosen := choose.member with inhabited84  have parts := finiteSubcovers.membership.forward with chosen85  exact parts.left8687theorem subcoverChoice.selected (X T C F A : Set)88  requires compact : ∀ B ∈ F, IsCompact(X, T, B)89  requires cover : OpenCover(T, ⋃(F), C)90  requires hA : A ∈ F91  shows subcoverChoice(X, T, C, F)(A) ∈ finiteSubcovers(C, A)92proof93  have value := subcoverChoice.value with compact, cover, hA94  rw value95  have compactA := compact with A, hA96  have below := union.subset_of_member with hA97  have coverA : OpenCover(T, A, C) := ⟨cover.left, (Subset.transitive with below, cover.right)⟩98  obtain ⟨G, hG, finiteG, covered⟩ := compactA.right with C, coverA99  have found : G ∈ finiteSubcovers(C, A) := finiteSubcovers.membership.backward with ⟨(powerset.membership_iff.backward with hG), finiteG, covered⟩100  have inhabited : Nonempty(finiteSubcovers(C, A)) := ⟨G, found⟩101  exact choose.member with inhabited102103theorem IsCompact.finite_union (X T F : Set)104  requires finite : Finite(F)105  requires compact : ∀ B ∈ F, IsCompact(X, T, B)106  shows IsCompact(X, T, ⋃(F))107proof108  constructor109  . apply union.subset110    intros B hB111    have compactB := compact with B, hB112    exact compactB.left113  . intros C cover114    have graph := subcoverChoice.function with compact, cover115    have imageFinite := Finite.function_image with graph, finite, (Subset.reflexive at F)116    witness ⋃(functionImage(subcoverChoice(X, T, C, F), F, 𝒫(C)))117    refine ⟨?_, ?_, ?_⟩118    . apply union.subset119      intros G hG120      have inside := functionImage.subset at subcoverChoice(X, T, C, F), F, 𝒫(C)121      exact powerset.membership_iff.forward with (inside with G, hG)122    . apply Finite.big_union with imageFinite123      intros G hG124      simp [functionImage.membership] at hG125      obtain ⟨hGP, B, hB, shape⟩ := hG126      have selected := subcoverChoice.selected with compact, cover, hB127      have parts := finiteSubcovers.membership.forward with selected128      rw shape129      exact parts.right.left130    . intros x hx131      obtain ⟨B, hB, hxB⟩ := union.membership.forward with hx132      have selected := subcoverChoice.selected with compact, cover, hB133      have parts := finiteSubcovers.membership.forward with selected134      have covered := parts.right.right with x, hxB135      obtain ⟨U, hU, hxU⟩ := union.membership.forward with covered136      have imageMember := functionImage.value with graph, hB137      have inUnion := union.contains with imageMember, hU138      exact union.contains with inUnion, hxU139140-- A compact set meets a closed set in a compact set: add the complement141-- of the closed set to a cover of the intersection.142theorem IsCompact.intersection_closed (X T K C : Set)143  requires topology : IsTopology(X, T)144  requires compact : IsCompact(X, T, K)145  requires closed : IsClosed(X, T, C)146  shows IsCompact(X, T, K ∩ C)147proof148  have hKX := compact.left149  constructor150  . exact Subset.transitive with (intersection.subset_left at K, C), hKX151  . intros D cover152    have extendedOpen : insert(complement(X, C), D) ⊆ T153      intros U hU154      have split := insert.membership.forward with hU155      cases split with isComplement | inD156      . rw isComplement157        exact closed.right158      . exact cover.left with U, inD159    have extendedCover : K ⊆ ⋃(insert(complement(X, C), D))160      intros k hk161      have hkX := hKX with k, hk162      have split : k ∈ C ∨ ¬k ∈ C by tauto163      cases split with inC | outside164      . have inBoth : k ∈ K ∩ C := intersection.membership.backward with ⟨hk, inC⟩165        have covered := cover.right with k, inBoth166        obtain ⟨U, hU, hkU⟩ := union.membership.forward with covered167        have found : U ∈ insert(complement(X, C), D)168          apply insert.membership.backward169          right170          exact hU171        exact union.contains with found, hkU172      . have inComplement : k ∈ complement(X, C) := complement.membership.backward with ⟨hkX, outside⟩173        have found : complement(X, C) ∈ insert(complement(X, C), D)174          apply insert.membership.backward175          left176          rfl177        exact union.contains with found, inComplement178    obtain ⟨F, hF, finiteF, coveredK⟩ := compact.right with insert(complement(X, C), D), ⟨extendedOpen, extendedCover⟩179    witness F ∖ {complement(X, C)}180    refine ⟨?_, (Finite.subset with finiteF, (difference.subset_left at F, {complement(X, C)})), ?_⟩181    . intros U hU182      have parts := difference.singleton_membership.forward with hU183      have split := insert.membership.forward with (hF with U, parts.left)184      cases split with isComplement | inD185      . exfalso186        exact parts.right with isComplement187      . exact inD188    . intros k hk189      have inBoth := intersection.membership.forward with hk190      have covered := coveredK with k, inBoth.left191      obtain ⟨U, hU, hkU⟩ := union.membership.forward with covered192      have kept : U ∈ F ∖ {complement(X, C)}193        apply difference.singleton_membership.backward194        refine ⟨hU, ?_⟩195        intro isComplement196        rw isComplement at hkU197        have away := complement.membership.forward with hkU198        exact away.right with inBoth.right199      exact union.contains with kept, hkU200201-- Separating a compact set from a set D: when every point of K has an202-- open neighbourhood disjoint from an open set around D, so does K.203204def separators (T D U : Set) : Set := { V ∈ T | D ⊆ V ∧ Disjoint(U, V) }205def separatingOpens (T D : Set) : Set := { U ∈ T | Nonempty(separators(T, D, U)) }206207defgraph separatorChoice (T D F : Set) (U ∈ F) : T := choose(separators(T, D, U))208requires inside : F ⊆ separatingOpens(T, D)209proof210  have hU := inside with U, member211  have parts := separatingOpens.membership.forward with hU212  have chosen := choose.member with parts.right213  have chosenParts := separators.membership.forward with chosen214  exact chosenParts.left215216theorem separatorChoice.selected (T D F U : Set)217  requires inside : F ⊆ separatingOpens(T, D)218  requires hU : U ∈ F219  shows separatorChoice(T, D, F)(U) ∈ separators(T, D, U)220proof221  have value := separatorChoice.value with inside, hU222  rw value223  have hU2 := inside with U, hU224  have parts := separatingOpens.membership.forward with hU2225  exact choose.member with parts.right226227theorem IsCompact.separate (X T K D : Set)228  requires topology : IsTopology(X, T)229  requires compact : IsCompact(X, T, K)230  requires hD : D ⊆ X231  requires separated : ∀ k ∈ K, ∃ U ∈ T, ∃ V ∈ T, k ∈ U ∧ D ⊆ V ∧ Disjoint(U, V)232  shows ∃ U ∈ T, ∃ V ∈ T, K ⊆ U ∧ D ⊆ V ∧ Disjoint(U, V)233proof234  have coverOpen : separatingOpens(T, D) ⊆ T235    intros U hU236    have parts := separatingOpens.membership.forward with hU237    exact parts.left238  have covers : K ⊆ ⋃(separatingOpens(T, D))239    intros k hk240    obtain ⟨U, hU, V, hV, hkU, inside, disjoint⟩ := separated with k, hk241    have found : V ∈ separators(T, D, U) := separators.membership.backward with ⟨hV, inside, disjoint⟩242    have inhabited : Nonempty(separators(T, D, U)) := ⟨V, found⟩243    have opens : U ∈ separatingOpens(T, D) := separatingOpens.membership.backward with ⟨hU, inhabited⟩244    exact union.contains with opens, hkU245  obtain ⟨F, hF, finiteF, coveredK⟩ := compact.right with separatingOpens(T, D), ⟨coverOpen, covers⟩246  have split : Nonempty(F) ∨ ¬Nonempty(F) by tauto247  cases split with inhabited | empty248  . have graph := separatorChoice.function with hF249    have openUnion := IsTopology.union with topology, (Subset.transitive with hF, coverOpen)250    have imageInside := functionImage.subset at separatorChoice(T, D, F), F, T251    have imageFinite := Finite.function_image with graph, finiteF, (Subset.reflexive at F)252    obtain ⟨U0, hU0⟩ := inhabited253    have firstMember := functionImage.value with graph, hU0254    have imageInhabited : Nonempty(functionImage(separatorChoice(T, D, F), F, T)) := ⟨separatorChoice(T, D, F)(U0), firstMember⟩255    have openMeet := IsTopology.finite_intersection with topology, imageFinite, imageInside, imageInhabited256    refine ⟨⋃(F), openUnion, ⋂(functionImage(separatorChoice(T, D, F), F, T)), openMeet, coveredK, ?_, ?_⟩257    . apply familyIntersection.greatest with imageInhabited258      intros V hV259      simp [functionImage.membership] at hV260      obtain ⟨hVT, U, hU, shape⟩ := hV261      have selected := separatorChoice.selected with hF, hU262      have parts := separators.membership.forward with selected263      rw shape264      exact parts.right.left265    . apply Disjoint.iff.backward266      intros x hx hxMeet267      obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx268      have meetParts := familyIntersection.membership.forward with hxMeet269      have imageMember := functionImage.value with graph, hU270      have hxV := meetParts.right with separatorChoice(T, D, F)(U), imageMember271      have selected := separatorChoice.selected with hF, hU272      have parts := separators.membership.forward with selected273      have separatedUV := Disjoint.iff.forward with parts.right.right274      exact separatedUV with x, hxU, hxV275  . have equal : F = ∅276      by_contra different277      apply empty278      exact Nonempty.of_ne_empty with different279    rw [equal, union.empty] at coveredK280    refine ⟨∅, (IsTopology.empty with topology), X, (IsTopology.whole with topology), coveredK, hD, ?_⟩281    exact Disjoint.empty_left at X282283-- In a Hausdorff space a compact set and a point outside it have284-- disjoint open neighbourhoods, so compact sets are closed.285286theorem IsCompact.hausdorff_separated (X T K x : Set)287  requires topology : IsTopology(X, T)288  requires hausdorff : IsHausdorff(X, T)289  requires compact : IsCompact(X, T, K)290  requires hx : x ∈ X291  requires away : ¬x ∈ K292  shows ∃ U ∈ T, ∃ V ∈ T, K ⊆ U ∧ x ∈ V ∧ Disjoint(U, V)293proof294  have singletonInside : {x} ⊆ X := singleton.subset_iff.backward with hx295  have separated : ∀ k ∈ K, ∃ U ∈ T, ∃ V ∈ T, k ∈ U ∧ {x} ⊆ V ∧ Disjoint(U, V)296    intros k hk297    have hkX := compact.left with k, hk298    have distinct : k ≠ x299      intro same300      apply away301      rw ← same302      exact hk303    obtain ⟨U, hU, V, hV, hkU, hxV, disjoint⟩ := hausdorff with k, hkX, x, hx, distinct304    have inside : {x} ⊆ V := singleton.subset_iff.backward with hxV305    exact ⟨U, hU, V, hV, hkU, inside, disjoint⟩306  obtain ⟨U, hU, V, hV, coverK, inside, disjoint⟩ := IsCompact.separate with topology, compact, singletonInside, separated307  have hxV := singleton.subset_iff.forward with inside308  exact ⟨U, hU, V, hV, coverK, hxV, disjoint⟩309310def avoiding (T K : Set) : Set := { V ∈ T | Disjoint(V, K) }311312theorem IsCompact.hausdorff_closed (X T K : Set)313  requires topology : IsTopology(X, T)314  requires hausdorff : IsHausdorff(X, T)315  requires compact : IsCompact(X, T, K)316  shows IsClosed(X, T, K)317proof318  constructor319  . exact compact.left320  . have avoidingOpen : avoiding(T, K) ⊆ T321      intros V hV322      have parts := avoiding.membership.forward with hV323      exact parts.left324    have isOpen := IsTopology.union with topology, avoidingOpen325    have equal : complement(X, K) = ⋃(avoiding(T, K))326      ext x327      constructor328      . intro hx329        have parts := complement.membership.forward with hx330        obtain ⟨U, hU, V, hV, coverK, hxV, disjoint⟩ := IsCompact.hausdorff_separated with topology, hausdorff, compact, parts.left, parts.right331        have symmetric := Disjoint.symmetric with disjoint332        have disjointK := Disjoint.of_subset_right with symmetric, coverK333        have found : V ∈ avoiding(T, K) := avoiding.membership.backward with ⟨hV, disjointK⟩334        exact union.contains with found, hxV335      . intro hx336        obtain ⟨V, hV, hxV⟩ := union.membership.forward with hx337        have parts := avoiding.membership.forward with hV338        have inside := IsTopology.subset with topology, parts.left339        have separated := Disjoint.iff.forward with parts.right340        apply complement.membership.backward341        exact ⟨(inside with x, hxV), (separated with x, hxV)⟩342    rwa equal343344-- In a compact Hausdorff space the compact sets are exactly the closed345-- sets.346theorem IsCompact.hausdorff_iff_closed (X T K : Set)347  requires topology : IsTopology(X, T)348  requires hausdorff : IsHausdorff(X, T)349  requires compact : IsCompact(X, T, X)350  shows IsCompact(X, T, K) ↔ IsClosed(X, T, K)351proof352  constructor353  . intro compactK354    exact IsCompact.hausdorff_closed with topology, hausdorff, compactK355  . intro closed356    exact IsCompact.closed_subset with topology, compact, closed, closed.left357358theorem IsCompact.hausdorff_intersection (X T K L : Set)359  requires topology : IsTopology(X, T)360  requires hausdorff : IsHausdorff(X, T)361  requires compactK : IsCompact(X, T, K)362  requires compactL : IsCompact(X, T, L)363  shows IsCompact(X, T, K ∩ L)364proof365  have closed := IsCompact.hausdorff_closed with topology, hausdorff, compactL366  exact IsCompact.intersection_closed with topology, compactK, closed367368-- Two disjoint compact sets in a Hausdorff space have disjoint open369-- neighbourhoods.370theorem IsCompact.hausdorff_separate (X T K L : Set)371  requires topology : IsTopology(X, T)372  requires hausdorff : IsHausdorff(X, T)373  requires compactK : IsCompact(X, T, K)374  requires compactL : IsCompact(X, T, L)375  requires disjoint : Disjoint(K, L)376  shows ∃ U ∈ T, ∃ V ∈ T, K ⊆ U ∧ L ⊆ V ∧ Disjoint(U, V)377proof378  have separatedKL := Disjoint.iff.forward with disjoint379  have separated : ∀ k ∈ K, ∃ U ∈ T, ∃ V ∈ T, k ∈ U ∧ L ⊆ V ∧ Disjoint(U, V)380    intros k hk381    have hkX := compactK.left with k, hk382    have away := separatedKL with k, hk383    obtain ⟨U, hU, V, hV, coverL, hkV, disjointUV⟩ := IsCompact.hausdorff_separated with topology, hausdorff, compactL, hkX, away384    have symmetric := Disjoint.symmetric with disjointUV385    exact ⟨V, hV, U, hU, hkV, coverL, symmetric⟩386  exact IsCompact.separate with topology, compactK, compactL.left, separated387388theorem IsCompact.hausdorff_regular (X T : Set)389  requires topology : IsTopology(X, T)390  requires hausdorff : IsHausdorff(X, T)391  requires compact : IsCompact(X, T, X)392  shows RegularSpace(X, T)393proof394  intros x hx C closedC away395  have compactC := IsCompact.closed_subset with topology, compact, closedC, closedC.left396  obtain ⟨U, hU, V, hV, coverC, hxV, disjoint⟩ := IsCompact.hausdorff_separated with topology, hausdorff, compactC, hx, away397  have symmetric := Disjoint.symmetric with disjoint398  exact ⟨V, hV, U, hU, hxV, coverC, symmetric⟩399400theorem IsCompact.hausdorff_normal (X T : Set)401  requires topology : IsTopology(X, T)402  requires hausdorff : IsHausdorff(X, T)403  requires compact : IsCompact(X, T, X)404  shows NormalSpace(X, T)405proof406  intros C closedC D closedD disjoint407  have compactC := IsCompact.closed_subset with topology, compact, closedC, closedC.left408  have compactD := IsCompact.closed_subset with topology, compact, closedD, closedD.left409  exact IsCompact.hausdorff_separate with topology, hausdorff, compactC, compactD, disjoint410411-- The finite intersection property: every finite nonempty subfamily has412-- a common point. In a compact space a family of closed sets with this413-- property has a common point, and that characterises compactness.414415predicate FiniteIntersectionProperty (S : Set) :=416  ∀ F, F ⊆ S → Finite(F) → Nonempty(F) → Nonempty(⋂(F))417418defgraph complementMap (X G : Set) (g ∈ G) : 𝒫(X) := complement(X, g)419proof420  exact powerset.membership_iff.backward with (complement.subset at X, g)421422theorem complementMap.selected (X S G g : Set)423  requires inside : ∀ C ∈ S, C ⊆ X424  requires hG : G ⊆ complements(X, S)425  requires hg : g ∈ G426  shows complementMap(X, G)(g) ∈ S ∧ complement(X, complementMap(X, G)(g)) = g427proof428  have value := complementMap.value at X, G, g with hg429  rw value430  obtain ⟨C, hC, shape⟩ := complements.membership.forward with (hG with g, hg)431  have hCX := inside with C, hC432  have fold : complement(X, C) = X ∖ C433    unfold complement434    rfl435  rw ← fold at shape436  rw ← shape437  have double := complement.complement with hCX438  rw double439  constructor440  . exact hC441  . rfl442443theorem IsCompact.closed_family_meets (X T S : Set)444  requires topology : IsTopology(X, T)445  requires compact : IsCompact(X, T, X)446  requires closed : ∀ C ∈ S, IsClosed(X, T, C)447  requires fip : FiniteIntersectionProperty(S)448  requires nonempty : Nonempty(S)449  shows Nonempty(⋂(S))450proof451  have inside : ∀ C ∈ S, C ⊆ X452    intros C hC453    have closedC := closed with C, hC454    exact closedC.left455  by_contra none456  have empty : ⋂(S) = ∅457    by_contra different458    apply none459    exact Nonempty.of_ne_empty with different460  have coverOpen : complements(X, S) ⊆ T461    intros U hU462    obtain ⟨C, hC, shape⟩ := complements.membership.forward with hU463    rw ← shape464    have closedC := closed with C, hC465    have isOpen := closedC.right466    unfold complement at isOpen467    exact isOpen468  have covers : X ⊆ ⋃(complements(X, S))469    have demorgan := complements.intersection at X, S with nonempty470    rw [← demorgan, empty, complement.empty]471    exact Subset.reflexive at X472  obtain ⟨G, hG, finiteG, coveredX⟩ := compact.right with complements(X, S), ⟨coverOpen, covers⟩473  have graph := complementMap.function at X, G474  have values : ∀ g ∈ G, complementMap(X, G)(g) ∈ S475    intros g hg476    have selected := complementMap.selected with inside, hG, hg477    exact selected.left478  have graphS := FunctionBetween.codomain_of_values with graph, values479  have imageFinite := Finite.function_image with graphS, finiteG, (Subset.reflexive at G)480  have imageInside := functionImage.subset at complementMap(X, G), G, S481  have inhabitedG : Nonempty(G)482    by_contra emptyG483    have equal : G = ∅484      by_contra different485      apply emptyG486      exact Nonempty.of_ne_empty with different487    rw [equal, union.empty] at coveredX488    obtain ⟨C, hC⟩ := nonempty489    have singletonInside : {C} ⊆ S := singleton.subset_iff.backward with hC490    have meets := fip with {C}, singletonInside, (Finite.singleton at C), (Nonempty.singleton at C)491    rw familyIntersection.singleton at meets492    obtain ⟨x, hx⟩ := meets493    have hxX := inside with C, hC, x, hx494    have inEmpty := coveredX with x, hxX495    exact empty.membership with x, inEmpty496  obtain ⟨g0, hg0⟩ := inhabitedG497  have firstMember := functionImage.value with graphS, hg0498  have imageInhabited : Nonempty(functionImage(complementMap(X, G), G, S)) := ⟨complementMap(X, G)(g0), firstMember⟩499  have meets := fip with functionImage(complementMap(X, G), G, S), imageInside, imageFinite, imageInhabited500  obtain ⟨x, hx⟩ := meets501  have meetParts := familyIntersection.membership.forward with hx502  have inFirst := meetParts.right with complementMap(X, G)(g0), firstMember503  have selected0 := complementMap.selected with inside, hG, hg0504  have hxX := inside with complementMap(X, G)(g0), selected0.left, x, inFirst505  have covered := coveredX with x, hxX506  obtain ⟨g, hg, hxg⟩ := union.membership.forward with covered507  have selected := complementMap.selected with inside, hG, hg508  have imageMember := functionImage.value with graphS, hg509  have inC := meetParts.right with complementMap(X, G)(g), imageMember510  have shape := selected.right511  rw ← shape at hxg512  have away := complement.membership.forward with hxg513  exact away.right with inC514515theorem IsCompact.of_closed_families (X T : Set)516  requires topology : IsTopology(X, T)517  requires meets : ∀ S, (∀ C ∈ S, IsClosed(X, T, C)) → FiniteIntersectionProperty(S) →518    Nonempty(S) → Nonempty(⋂(S))519  shows IsCompact(X, T, X)520proof521  constructor522  . exact Subset.reflexive at X523  . intros C cover524    by_contra none525    have split : Nonempty(C) ∨ ¬Nonempty(C) by tauto526    cases split with inhabitedC | emptyC527    . have inside : ∀ U ∈ C, U ⊆ X528        intros U hU529        exact IsTopology.subset with topology, (cover.left with U, hU)530      have closedFamily : ∀ D ∈ complements(X, C), IsClosed(X, T, D)531        intros D hD532        obtain ⟨U, hU, shape⟩ := complements.membership.forward with hD533        have fold : complement(X, U) = X ∖ U534          unfold complement535          rfl536        rw [← shape, ← fold]537        exact Open.complement_closed with topology, (cover.left with U, hU)538      have fip : FiniteIntersectionProperty(complements(X, C))539        intros F hF finiteF inhabitedF540        by_contra noPoint541        apply none542        have graph := complementMap.function at X, F543        have values : ∀ f ∈ F, complementMap(X, F)(f) ∈ C544          intros f hf545          have selected := complementMap.selected with inside, hF, hf546          exact selected.left547        have graphC := FunctionBetween.codomain_of_values with graph, values548        witness functionImage(complementMap(X, F), F, C)549        refine ⟨(functionImage.subset at complementMap(X, F), F, C), (Finite.function_image with graphC, finiteF, (Subset.reflexive at F)), ?_⟩550        intros x hx551        have characterization := familyIntersection.membership_of_nonempty at x, F with inhabitedF552        have notAll : ¬(∀ f ∈ F, x ∈ f)553          intro all554          apply noPoint555          exact ⟨x, (characterization.backward with all)⟩556        by_contra notCovered557        apply notAll558        intros f hf559        by_contra outside560        apply notCovered561        have selected := complementMap.selected with inside, hF, hf562        have imageMember := functionImage.value with graphC, hf563        have inOriginal : x ∈ complementMap(X, F)(f)564          by_contra notIn565          apply outside566          rw ← selected.right567          exact complement.membership.backward with ⟨hx, notIn⟩568        exact union.contains with imageMember, inOriginal569      obtain ⟨U, hU⟩ := inhabitedC570      have found : X ∖ U ∈ complements(X, C) := complements.membership.backward with ⟨U, hU, rfl⟩571      have inhabitedS : Nonempty(complements(X, C)) := ⟨X ∖ U, found⟩572      obtain ⟨x, hx⟩ := meets with complements(X, C), closedFamily, fip, inhabitedS573      have characterization := familyIntersection.membership_of_nonempty at x, complements(X, C) with inhabitedS574      have all := characterization.forward with hx575      have inFirst := all with X ∖ U, found576      have firstParts := difference.membership.forward with inFirst577      have covered := cover.right with x, firstParts.left578      obtain ⟨V, hV, hxV⟩ := union.membership.forward with covered579      have foundV : X ∖ V ∈ complements(X, C) := complements.membership.backward with ⟨V, hV, rfl⟩580      have inV := all with X ∖ V, foundV581      have partsV := difference.membership.forward with inV582      exact partsV.right with hxV583    . apply none584      have equal : C = ∅585        by_contra different586        apply emptyC587        exact Nonempty.of_ne_empty with different588      have covered := cover.right589      rw equal at covered590      witness ∅591      exact ⟨(empty.subset at C), Finite.empty, covered⟩592593theorem IsCompact.iff_closed_families (X T : Set)594  requires topology : IsTopology(X, T)595  shows IsCompact(X, T, X) ↔ ∀ S, (∀ C ∈ S, IsClosed(X, T, C)) →596    FiniteIntersectionProperty(S) → Nonempty(S) → Nonempty(⋂(S))597proof598  constructor599  . intros compact S closed fip nonempty600    exact IsCompact.closed_family_meets with topology, compact, closed, fip, nonempty601  . intro meets602    exact IsCompact.of_closed_families with topology, meets603