Grace/Cumulus/Cardinal/Counting.g17

Open in Workbench Download source

Imports

Enumeration

Declarations

Source

1-- Cardinality under bijections, insertion and removal of a point, the2-- empty set as the set of size zero, differences of finite sets, and3-- induction over finite subsets of a set (ZF).4-- 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.Cardinal.Counting10import Enumeration1112theorem cardinality.bijective (A B f : Set)13  requires finite : Finite(A)14  requires bijective : BijectiveBetween(f, A, B)15  shows cardinality(A) = cardinality(B)16proof17  obtain ⟨natural, g, enumeration⟩ := cardinality.correct with finite18  have inverse := converse.bijective with bijective19  have composed := compose.bijective at g, converse(f, A, B), B, A, cardinality(A) with *20  have other : HasCardinality(B, cardinality(A))21    unfold HasCardinality22    refine ⟨natural, ?_⟩23    unfold Equipotent24    refine ⟨compose(g, converse(f, A, B), B, A, cardinality(A)), composed⟩25  symm26  exact cardinality.eq_of_has with other2728theorem cardinality.insert (A a : Set)29  requires finite : Finite(A)30  requires fresh : ¬(a ∈ A)31  shows cardinality(insert(a, A)) = succ(cardinality(A))32proof33  obtain ⟨natural, f, enumeration⟩ := cardinality.correct with finite34  have newIndex := membership.irreflexive at cardinality(A)35  have extended := adjoinMap.bijective with *36  have successor := natural.successor_as_insert with natural37  rw ← successor at extended38  have next := Naturals.constructor.succ with natural39  have cardinal : HasCardinality(insert(a, A), succ(cardinality(A)))40    unfold HasCardinality41    refine ⟨next, ?_⟩42    unfold Equipotent43    refine ⟨adjoinMap(f, a, cardinality(A)), extended⟩44  exact cardinality.eq_of_has with cardinal4546theorem Finite.difference (A B : Set)47  requires finite : Finite(A)48  shows Finite(A ∖ B)49proof50  exact Finite.subset with finite, (difference.subset_left at A, B)5152theorem cardinality.remove (A a : Set)53  requires finite : Finite(A)54  requires member : a ∈ A55  shows cardinality(A) = succ(cardinality(A ∖ {a}))56proof57  have smaller := Finite.difference at A, {a} with finite58  have fresh : ¬(a ∈ A ∖ {a}) by simp [difference.membership, singleton.membership]59  have restored := insert.restore with member60  have count := cardinality.insert with *61  rwa restored at count6263-- The same counts in the form n + 1, and with the point adjoined as a union.64theorem cardinality.insert_add_one (A a : Set)65  requires finite : Finite(A)66  requires fresh : ¬a ∈ A67  shows cardinality(insert(a, A)) = cardinality(A) + 168proof69  have inserted := cardinality.insert with finite, fresh70  have natA := HasCardinality.natural with (cardinality.correct with finite)71  have one := add.right_one at cardinality(A)72  rw [inserted, one]73  rfl7475theorem cardinality.union_singleton (A a : Set)76  requires finite : Finite(A)77  requires fresh : ¬a ∈ A78  shows cardinality(A ∪ {a}) = cardinality(A) + 179proof80  have asInsert : A ∪ {a} = insert(a, A)81    unfold insert82    exact union2.commutative at A, {a}83  rw asInsert84  exact cardinality.insert_add_one with finite, fresh8586theorem cardinality.remove_add_one (A a : Set)87  requires finite : Finite(A)88  requires member : a ∈ A89  shows cardinality(A) = cardinality(A ∖ {a}) + 190proof91  have removed := cardinality.remove with finite, member92  have restFinite := Finite.difference at A, {a} with finite93  have restNat := HasCardinality.natural94    with (cardinality.correct with restFinite)95  have one := add.right_one at cardinality(A ∖ {a})96  rw [removed, one]97  rfl9899-- A finite set of size zero is empty.100theorem HasCardinality.empty_of_zero (A : Set)101  requires counted : HasCardinality(A, 0)102  shows A = ∅103proof104  rcases counted with ⟨natural, f, bijective⟩105  have function := Bijective.injective with bijective106  have graph := Injective.function with function107  have subset : A ⊆ ∅108    intros a member109    obtain ⟨y, inZero, related⟩ :=110      FunctionBetween.exists_value at f, A, 0, a with *111    exfalso112    rw nat.zero at inZero113    exact set.empty with inZero114  have reverse := empty.subset at A115  exact Subset.antisymmetric with *116117theorem cardinality.eq_empty_of_zero (A : Set)118  requires finite : Finite(A)119  requires zero : cardinality(A) = 0120  shows A = ∅121proof122  have counted := cardinality.correct with finite123  rw zero at counted124  exact HasCardinality.empty_of_zero with counted125126-- A set of size k + 1 is a set of size k with one element put back.127theorem cardinality.exists_remove (F : Set) (k : Nat)128  requires finite : Finite(F)129  requires size : cardinality(F) = succ(k)130  shows ∃ e ∈ F, cardinality(F ∖ {e}) = k ∧ (F ∖ {e}) ∪ {e} = F131proof132  have inhabited : ∃ e, e ∈ F133    by_contra none134    have empty : F = ∅135      ext y136      constructor137      . intro hy138        exfalso139        exact none with ⟨y, hy⟩140      . intro hy141        exfalso142        exact set.empty with hy143    rw [empty, cardinality.empty] at size144    exact Naturals.disjoint.zero.succ at k with size145  obtain ⟨e, he⟩ := inhabited146  have removed := cardinality.remove with finite, he147  rw size at removed148  have restored : (F ∖ {e}) ∪ {e} = F149    ext y150    simp151  refine ⟨e, he, _, restored⟩152  symm153  exact Naturals.injective.succ with removed154155-- Induction over the finite subsets of E, by the size of the subset: a156-- family S of sets containing ∅ and closed under adjoining a fresh point of157-- E to a finite member contains every finite subset of E.158theorem Finite.induction_of_size (E S : Set, n : Nat)159  requires base : ∅ ∈ S160  requires step : ∀ F ⊆ E, Finite(F) → ∀ a ∈ E, a ∉ F → F ∈ S →161    F ∪ {a} ∈ S162  shows ∀ F ⊆ E, Finite(F) → cardinality(F) = n → F ∈ S163proof164  induction n165  | zero =>166    intros F bound finite size167    have empty : F = ∅168      ext y169      constructor170      . intro hy171        exfalso172        have removed := cardinality.remove with finite, hy173        rw size at removed174        exact Naturals.disjoint.zero.succ at cardinality(F ∖ {y}) with removed175      . intro hy176        exfalso177        exact set.empty with hy178    rw empty179    exact base180  | succ(k) using ih =>181    intros F bound finite size182    obtain ⟨e, he, restSize, restored⟩ :=183      cardinality.exists_remove with finite, size184    have restSubset := difference.subset_left at F, {e}185    have restBound := Subset.transitive with restSubset, bound186    have restFinite := Finite.subset with finite, restSubset187    have rest := ih with F ∖ {e}, restBound, restFinite, restSize188    have fresh : e ∉ F ∖ {e} by simp189    have next := step with F ∖ {e}, restBound, restFinite, e,190      (bound with e, he), fresh, rest191    rw restored at next192    exact next193194theorem Finite.induction (E S : Set)195  requires base : ∅ ∈ S196  requires step : ∀ F ⊆ E, Finite(F) → ∀ a ∈ E, a ∉ F → F ∈ S →197    F ∪ {a} ∈ S198  shows ∀ F ⊆ E, Finite(F) → F ∈ S199proof200  intros F bound finite201  have correct := cardinality.correct with finite202  have natural := correct.left203  have size : cardinality(F) = cardinality(F) by rfl204  exact Finite.induction_of_size at E, S, cardinality(F)205    with natural, base, step, F, bound, finite, size206