Grace/Cumulus/Cardinal/FiniteSubsets.g17

Open in Workbench Download source

Imports

FiniteImage

Declarations

• insertSubset defgraph
• Finite.powerset_insert theorem derivation
• listSupport.finite_powerset theorem derivation
• Finite.powerset theorem derivation
• listSupport.maximal_extension theorem derivation
• Finite.maximal_extension theorem derivation

Source

1-- Finite powersets and maximal members of finite families, in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.FiniteSubsets8import FiniteImage910defgraph insertSubset (A x : Set) (S ∈ 𝒫(A)) : 𝒫(insert(x, A)) := insert(x, S)11proof12  apply powerset.membership_iff.backward at insert(x, S), insert(x, A)13  have subset := powerset.membership_iff.forward at S, A with *14  settle with Subset, insert.membership1516theorem Finite.powerset_insert (A x : Set)17  requires finite : Finite(𝒫(A))18  shows Finite(𝒫(insert(x, A)))19proof20  have function := insertSubset.function at A, x21  have reflexive : 𝒫(A) ⊆ 𝒫(A) by simp22  have image := Finite.function_image with function, finite, reflexive23  have combined := Finite.union with finite, image24  have covered : 𝒫(insert(x, A)) ⊆ 𝒫(A) ∪ functionImage(insertSubset(A, x), 𝒫(A), 𝒫(insert(x, A)))25    intros S member26    have subset := powerset.membership_iff.forward with member27    have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto28    cases alternatives with present | absent29    . have rest : S ∖ {x} ⊆ A by simp30      have restIn := powerset.membership_iff.backward with rest31      have restored : insert(x, S ∖ {x}) = S32        ext y33        simp34      have value := insertSubset.value at A, x, S ∖ {x} with restIn35      have inImage : S ∈ functionImage(insertSubset(A, x), 𝒫(A), 𝒫(insert(x, A)))36        apply functionImage.membership.backward37        refine ⟨member, S ∖ {x}, restIn, ?_⟩38        cc39      simp40    . have smaller : S ⊆ A41        intros y hy42        have inInsert := subset with y, hy43        simp44      have old := powerset.membership_iff.backward with smaller45      simp46  exact Finite.subset with combined, covered4748theorem listSupport.finite_powerset (C : Set) (xs : List(C))49  shows Finite(𝒫(listSupport{C}(xs)))50proof51  induction xs52  | List.nil =>53    rw listSupport54    have bounded : 𝒫(∅) ⊆ {∅}55      intros S member56      have subset := powerset.membership_iff.forward with member57      have reverse := empty.subset at S58      have equal := Subset.antisymmetric with subset, reverse59      exact singleton.membership.backward with equal60    have finite := Finite.singleton at ∅61    exact Finite.subset with finite, bounded62  | List.cons(x, tail) using ih =>63    rw listSupport64    exact Finite.powerset_insert with *6566theorem Finite.powerset (A : Set)67  requires finite : Finite(A)68  shows Finite(𝒫(A))69proof70  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite71  have bound := listSupport.finite_powerset with list72  have included := powerset.monotone with covers73  exact Finite.subset with bound, included7475-- Scan a finite family, replacing the current member only by a larger one.76theorem listSupport.maximal_extension (F : Set) (xs : List(F))77  shows ∀ S ∈ F, ∃ M ∈ F, S ⊆ M ∧ (∀ T ∈ listSupport{F}(xs), M ⊆ T → T = M)78proof79  induction xs80  | List.nil =>81    intros S member82    refine ⟨S, member, ?_⟩83    constructor84    . settle with Subset85    . intros T inList contains86      rw listSupport at inList87      exfalso88      exact set.empty with inList89  | List.cons(x, tail) using ih =>90    intros S member91    obtain ⟨M, inFamily, extends, maximal⟩ := ih with S, member92    have alternatives : M ⊆ x ∨ ¬(M ⊆ x) by tauto93    cases alternatives with larger | incomparable94    . have xIn : x ∈ F95        assumption96      have extension := Subset.transitive with extends, larger97      refine ⟨x, xIn, extension, ?_⟩98      intros T inList contains99      rw listSupport at inList100      have casesT := insert.membership.forward with inList101      cases casesT with equal | inTail102      . exact equal103      . have includes := Subset.transitive with larger, contains104        have equal := maximal with T, inTail, includes105        have reverse : x ⊆ M by simp106        have same := Subset.antisymmetric with larger, reverse107        cc108    . refine ⟨M, inFamily, extends, ?_⟩109      intros T inList contains110      rw listSupport at inList111      have casesT := insert.membership.forward with inList112      cases casesT with equal | inTail113      . exfalso114        rw equal at contains115        exact incomparable with contains116      . exact maximal with T, inTail, contains117118theorem Finite.maximal_extension (F S : Set)119  requires finite : Finite(F)120  requires member : S ∈ F121  shows ∃ M ∈ F, S ⊆ M ∧ (∀ T ∈ F, M ⊆ T → T = M)122proof123  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite124  have scan := listSupport.maximal_extension with list125  obtain ⟨M, inFamily, extends, maximal⟩ := scan with S, member126  refine ⟨M, inFamily, extends, ?_⟩127  intros T inFamilyT contains128  have inList := covers with T, inFamilyT129  exact maximal with T, inList, contains130