Grace/Cumulus/Cardinal/PowersetCount.g17

Open in Workbench Download source

Imports

Counting · Sum · FiniteSubsets

Declarations

Source

1-- A set with n elements has 2^n subsets2-- 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.PowersetCount8import Counting9import Sum10import FiniteSubsets1112-- Subsets of insert(x, A) are sorted by whether they contain x: those that do13-- not are subsets of A, and those that do become subsets of A once x is14-- removed. The graph sends S to inl(S) or inr(S ∖ {x}) accordingly.15def powersetSplit (A x : Set) : Set :=16  { p ∈ 𝒫(insert(x, A)) × (𝒫(A) ⊎ 𝒫(A)) |17    ∃ S ∈ 𝒫(insert(x, A)), ((¬(x ∈ S) ∧ p = (S, inl(S))) ∨ (x ∈ S ∧ p = (S, inr(S ∖ {x})))) }1819theorem subset.without (A x S : Set)20  requires subset : S ⊆ insert(x, A)21  shows S ∖ {x} ⊆ A22proof23  simp2425theorem subset.absent (A x S : Set)26  requires subset : S ⊆ insert(x, A)27  requires absent : ¬(x ∈ S)28  shows S ⊆ A29proof30  simp3132theorem insert.remove_fresh (T x : Set)33  requires fresh : ¬(x ∈ T)34  shows insert(x, T) ∖ {x} = T35proof36  ext y37  simp3839theorem powersetSplit.relates_absent (A x S : Set)40  requires member : S ∈ 𝒫(insert(x, A))41  requires absent : ¬(x ∈ S)42  shows relates(powersetSplit(A, x), S, inl(S))43proof44  have subset := powerset.membership_iff.forward with member45  have small := subset.absent with *46  have inPower := powerset.membership_iff.backward with small47  unfold relates48  apply powersetSplit.membership.backward49  constructor50  . apply product.pair at S, inl(S), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A)51    . exact member52    . exact disjointSum.left with inPower53  . witness S54    constructor55    . exact member56    . left57      refine ⟨absent, rfl⟩5859theorem powersetSplit.relates_present (A x S : Set)60  requires member : S ∈ 𝒫(insert(x, A))61  requires present : x ∈ S62  shows relates(powersetSplit(A, x), S, inr(S ∖ {x}))63proof64  have subset := powerset.membership_iff.forward with member65  have rest := subset.without with *66  have inPower := powerset.membership_iff.backward with rest67  unfold relates68  apply powersetSplit.membership.backward69  constructor70  . apply product.pair at S, inr(S ∖ {x}), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A)71    . exact member72    . exact disjointSum.right with inPower73  . witness S74    constructor75    . exact member76    . right77      refine ⟨present, rfl⟩7879theorem powersetSplit.factors (A x u v : Set)80  requires h : relates(powersetSplit(A, x), u, v)81  shows u ∈ 𝒫(insert(x, A)) ∧ ((¬(x ∈ u) ∧ v = inl(u)) ∨ (x ∈ u ∧ v = inr(u ∖ {x})))82proof83  unfold relates at h84  simp [powersetSplit.membership] at h85  rcases h with ⟨bounded, S, inPower, shape⟩86  cases shape with absent | present87  . rcases absent with ⟨notIn, pair⟩88    obtain ⟨source, target⟩ := orderedPair.injective with pair89    rw ← source at inPower90    rw ← source at notIn91    rw ← source at target92    constructor93    . exact inPower94    . left95      refine ⟨notIn, target⟩96  . rcases present with ⟨isIn, pair⟩97    obtain ⟨source, target⟩ := orderedPair.injective with pair98    rw ← source at inPower99    rw ← source at isIn100    rw ← source at target101    constructor102    . exact inPower103    . right104      refine ⟨isIn, target⟩105106theorem powersetSplit.relation (A x : Set)107  shows RelationBetween(powersetSplit(A, x), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A))108proof109  simp [RelationBetween, Subset]110111theorem powersetSplit.total (A x : Set)112  shows TotalBetween(powersetSplit(A, x), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A))113proof114  intros S member115  have subset := powerset.membership_iff.forward with member116  have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto117  cases alternatives with present | absent118  . have rest := subset.without with *119    have inPower := powerset.membership_iff.backward with rest120    witness inr(S ∖ {x})121    constructor122    . exact disjointSum.right with inPower123    . exact powersetSplit.relates_present with *124  . have small := subset.absent with *125    have inPower := powerset.membership_iff.backward with small126    witness inl(S)127    constructor128    . exact disjointSum.left with inPower129    . exact powersetSplit.relates_absent with *130131theorem powersetSplit.functional (A x : Set)132  shows Functional(powersetSplit(A, x))133proof134  intros u v huv w huw135  have first := powersetSplit.factors with huv136  have second := powersetSplit.factors with huw137  rcases first with ⟨inPower, firstShape⟩138  rcases second with ⟨inPowerAgain, secondShape⟩139  cases firstShape with firstAbsent | firstPresent140  . rcases firstAbsent with ⟨absent, vShape⟩141    cases secondShape with secondAbsent | secondPresent142    . rcases secondAbsent with ⟨absentAgain, wShape⟩143      rw [vShape, wShape]144      rfl145    . rcases secondPresent with ⟨present, wShape⟩146      exfalso147      exact absent with present148  . rcases firstPresent with ⟨present, vShape⟩149    cases secondShape with secondAbsent | secondPresent150    . rcases secondAbsent with ⟨absent, wShape⟩151      exfalso152      exact absent with present153    . rcases secondPresent with ⟨presentAgain, wShape⟩154      rw [vShape, wShape]155      rfl156157theorem powersetSplit.function (A x : Set)158  shows powersetSplit(A, x) : 𝒫(insert(x, A)) → 𝒫(A) ⊎ 𝒫(A)159proof160  constructor161  . exact powersetSplit.relation at A, x162  . constructor163    . exact powersetSplit.functional at A, x164    . exact powersetSplit.total at A, x165166theorem powersetSplit.injective (A x : Set)167  shows InjectiveBetween(powersetSplit(A, x), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A))168proof169  constructor170  . exact powersetSplit.function at A, x171  . intros u hu v hv z hz huz hvz172    have first := powersetSplit.factors with huz173    have second := powersetSplit.factors with hvz174    rcases first with ⟨uPower, firstShape⟩175    rcases second with ⟨vPower, secondShape⟩176    cases firstShape with firstAbsent | firstPresent177    . rcases firstAbsent with ⟨uAbsent, zLeft⟩178      cases secondShape with secondAbsent | secondPresent179      . rcases secondAbsent with ⟨vAbsent, zLeftAgain⟩180        rw zLeft at zLeftAgain181        exact inl.injective with zLeftAgain182      . rcases secondPresent with ⟨vPresent, zRight⟩183        rw zLeft at zRight184        exfalso185        exact tags.disjoint with zRight186    . rcases firstPresent with ⟨uPresent, zRight⟩187      cases secondShape with secondAbsent | secondPresent188      . rcases secondAbsent with ⟨vAbsent, zLeft⟩189        rw zLeft at zRight190        exfalso191        exact tags.disjoint with zRight192      . rcases secondPresent with ⟨vPresent, zRightAgain⟩193        rw zRight at zRightAgain194        have sameRest := inr.injective with zRightAgain195        have restoreU := insert.restore with uPresent196        have restoreV := insert.restore with vPresent197        rw [← restoreU, ← restoreV, sameRest]198        rfl199200theorem powersetSplit.surjective (A x : Set)201  requires fresh : ¬(x ∈ A)202  shows SurjectiveBetween(powersetSplit(A, x), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A))203proof204  constructor205  . exact powersetSplit.function at A, x206  . intros v hv207    have shape := disjointSum.membership.forward with hv208    cases shape with leftShape | rightShape209    . obtain ⟨T, inPower, vShape⟩ := leftShape210      have subset := powerset.membership_iff.forward with inPower211      have larger : T ⊆ insert(x, A) by simp212      have member := powerset.membership_iff.backward with larger213      have absent : ¬(x ∈ T) by simp214      witness T215      constructor216      . exact member217      . rw vShape218        exact powersetSplit.relates_absent with *219    . obtain ⟨T, inPower, vShape⟩ := rightShape220      have subset := powerset.membership_iff.forward with inPower221      have larger : insert(x, T) ⊆ insert(x, A) by simp222      have member := powerset.membership_iff.backward with larger223      have present := insert.self at x, T224      have absent : ¬(x ∈ T) by simp225      have removed := insert.remove_fresh with absent226      have related := powersetSplit.relates_present with *227      rw removed at related228      witness insert(x, T)229      constructor230      . exact member231      . rw vShape232        exact related233234theorem powersetSplit.bijective (A x : Set)235  requires fresh : ¬(x ∈ A)236  shows BijectiveBetween(powersetSplit(A, x), 𝒫(insert(x, A)), 𝒫(A) ⊎ 𝒫(A))237proof238  simp [BijectiveBetween, powersetSplit.injective, powersetSplit.surjective]239240theorem Equipotent.powerset_insert (A x : Set)241  requires fresh : ¬(x ∈ A)242  shows 𝒫(insert(x, A)) ≃ 𝒫(A) ⊎ 𝒫(A)243proof244  simp [Equipotent, powersetSplit.bijective]245246-- Adding a fresh element doubles the number of subsets.247theorem HasCardinality.powerset_insert (A x m : Set)248  requires counted : HasCardinality(𝒫(A), m)249  requires fresh : ¬(x ∈ A)250  shows HasCardinality(𝒫(insert(x, A)), add(m, m))251proof252  have doubled := HasCardinality.disjointSum with *253  rcases doubled with ⟨natural, equivalent⟩254  have split := Equipotent.powerset_insert with *255  constructor256  . exact natural257  . exact Equipotent.transitive with *258259theorem HasCardinality.exists_member (A : Set, n : Nat)260  requires counted : HasCardinality(A, succ(n))261  shows ∃ a, a ∈ A262proof263  rcases counted with ⟨natural, f, bijective⟩264  obtain ⟨function, onto⟩ := Bijective.surjective with bijective265  have last := membership.self_successor at n with *266  obtain ⟨a, member, related⟩ := onto with n, last267  witness a268  exact member269270theorem powerset.empty271  shows 𝒫(∅) = {∅}272proof273  ext S274  constructor275  . intro member276    have subset := powerset.membership_iff.forward with member277    have reverse := empty.subset at S278    have equal := Subset.antisymmetric at S, ∅ with *279    exact singleton.membership.backward with equal280  . intro member281    have equal := singleton.membership.forward with member282    rw equal283    have reflexive := empty.subset at ∅284    exact powerset.membership_iff.backward with reflexive285286theorem HasCardinality.powerset_empty287  shows HasCardinality(𝒫(∅), 1)288proof289  constructor290  . exact Naturals.constructor.succ at 0 with Naturals.constructor.zero291  . rw powerset.empty292    exact Equipotent.singleton_one293294-- A set with n elements has 2^n subsets. Induction on n: remove an element,295-- count the subsets of the rest, and double.296theorem powerset.cardinality (A : Set) (n : Nat)297  requires counted : HasCardinality(A, n)298  shows HasCardinality(𝒫(A), 2 ^ n)299proof300  induction n generalizing A301  | zero =>302    intros A counted303    have empty := HasCardinality.empty_of_zero at A with counted304    rw [empty, pow.zero]305    exact HasCardinality.powerset_empty306  | succ(k) using ih =>307    intros A counted308    obtain ⟨a, member⟩ := HasCardinality.exists_member with counted309    have finite := Finite.from_cardinality with counted310    have count := cardinality.eq_of_has with counted311    have removal := cardinality.remove at A, a with *312    rw count at removal313    have subset := difference.subset_left at A, {a}314    have finiteRest := Finite.subset at A ∖ {a}, A with *315    obtain ⟨restNatural, restEquivalent⟩ := cardinality.correct with finiteRest316    have equal := Naturals.injective.succ with removal317    have restHas : HasCardinality(A ∖ {a}, k)318      unfold HasCardinality319      rw equal320      refine ⟨restNatural, restEquivalent⟩321    have powerRest := ih with A ∖ {a}, restHas322    have fresh : ¬(a ∈ A ∖ {a}) by simp [difference.membership, singleton.membership]323    have doubled := HasCardinality.powerset_insert at A ∖ {a}, a, 2 ^ k with *324    have restored := insert.restore with member325    rw restored at doubled326    have power : 2 ^ succ(k) = add(2 ^ k, 2 ^ k) by simp [pow.succ, mul.two_left]327    rwa power328