Grace/Cumulus/Combinatorics/Basics.g17

Open in Workbench Download source

Imports

Cardinal · Cardinal.Combinations · Nat.Subtraction

Declarations

Source

1-- Elementary cardinality facts for finite sets: the empty set, singletons,2-- pairs, inserting and removing a point, equipotence, and the counts of3-- products, disjoint sums, and power sets as equations about cardinality4-- 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.Combinatorics.Basics10import Cardinal11import Cardinal.Combinations12import Nat.Subtraction1314theorem HasCardinality.of_cardinality (A : Set) (n : Nat)15  requires finite : Finite(A)16  requires size : cardinality(A) = n17  shows HasCardinality(A, n)18proof19  have counted := cardinality.correct with finite20  rw size at counted21  exact counted2223theorem cardinality.eq_zero_iff (A : Set)24  requires finite : Finite(A)25  shows cardinality(A) = 0 ↔ A = ∅26proof27  constructor28  . intro zero29    have counted := cardinality.correct with finite30    rw zero at counted31    exact HasCardinality.empty_of_zero with counted32  . intro empty33    rw empty34    exact cardinality.empty3536theorem cardinality.positive_of_member (A a : Set)37  requires finite : Finite(A)38  requires member : a ∈ A39  shows 0 < cardinality(A)40proof41  have removed := cardinality.remove with finite, member42  have restFinite := Finite.subset with43    finite, (difference.subset_left at A, {a})44  have restNat := cardinality.nat with restFinite45  rw removed46  arith4748theorem cardinality.ne_zero_of_member (A a : Set)49  requires finite : Finite(A)50  requires member : a ∈ A51  shows cardinality(A) ≠ 052proof53  intro zero54  have iff := cardinality.eq_zero_iff with finite55  have empty := iff.forward with zero56  rw empty at member57  exact set.empty with member5859theorem cardinality.positive_iff_nonempty (A : Set)60  requires finite : Finite(A)61  shows Nonempty(A) ↔ 0 < cardinality(A)62proof63  constructor64  . intro nonempty65    obtain ⟨a, member⟩ := nonempty66    exact cardinality.positive_of_member with finite, member67  . intro positive68    apply Nonempty.of_ne_empty69    intro empty70    have iff := cardinality.eq_zero_iff with finite71    have zero := iff.backward with empty72    rw zero at positive73    have irreflexive := Less.irreflexive at 074    exact irreflexive with positive7576theorem cardinality.member_of_positive (A : Set)77  requires finite : Finite(A)78  requires positive : 0 < cardinality(A)79  shows ∃ a, a ∈ A80proof81  have iff := cardinality.positive_iff_nonempty with finite82  exact iff.backward with positive8384theorem cardinality.ne_zero_iff_nonempty (A : Set)85  requires finite : Finite(A)86  shows cardinality(A) ≠ 0 ↔ Nonempty(A)87proof88  constructor89  . intro nonzero90    apply Nonempty.of_ne_empty91    intro empty92    have iff := cardinality.eq_zero_iff with finite93    exact nonzero with (iff.backward with empty)94  . intro nonempty95    obtain ⟨a, member⟩ := nonempty96    exact cardinality.ne_zero_of_member with finite, member9798-- Inserting a point already present changes nothing.99theorem insert.eq_of_member (A a : Set)100  requires member : a ∈ A101  shows insert(a, A) = A102proof103  ext z104  simp105106theorem cardinality.insert_of_member (A a : Set)107  requires member : a ∈ A108  shows cardinality(insert(a, A)) = cardinality(A)109proof110  have same := insert.eq_of_member with member111  rw same112  rfl113114theorem cardinality.remove_sub_one (A a : Set)115  requires finite : Finite(A)116  requires member : a ∈ A117  shows cardinality(A ∖ {a}) = cardinality(A) - 1118proof119  have split := cardinality.remove_add_one with finite, member120  have restFinite := Finite.subset with121    finite, (difference.subset_left at A, {a})122  have restNat := cardinality.nat with restFinite123  rw split124  symm125  exact sub.add_right at cardinality(A ∖ {a}), 1126127theorem cardinality.remove_of_absent (A a : Set)128  requires absent : ¬a ∈ A129  shows cardinality(A ∖ {a}) = cardinality(A)130proof131  have same := difference.singleton_of_absent with absent132  rw same133  rfl134135theorem cardinality.pair (x y : Set)136  requires different : x ≠ y137  shows cardinality({x, y}) = 2138proof139  have shape : {x, y} = insert(x, {y})140    ext z141    simp142  have fresh : ¬x ∈ {y}143    intro member144    have equal := singleton.membership.forward with member145    exact different with equal146  have inserted := cardinality.insert at {y}, x with147    (Finite.singleton at y), fresh148  have one := cardinality.singleton at y149  rw [shape, inserted, one]150  compute151152theorem cardinality.pair_same (x : Set)153  shows cardinality({x, x}) = 1154proof155  have same : {x, x} = {x}156    ext z157    simp158  rw same159  exact cardinality.singleton at x160161-- A set with exactly one element is a singleton.162theorem cardinality.one_iff (A : Set)163  requires finite : Finite(A)164  shows cardinality(A) = 1 ↔ ∃ x, A = {x}165proof166  constructor167  . intro one168    have counted := cardinality.correct with finite169    rw one at counted170    obtain ⟨a, member⟩ := HasCardinality.exists_member at A, 0 with counted171    have split := cardinality.remove_add_one with finite, member172    have restFinite := Finite.subset with173      finite, (difference.subset_left at A, {a})174    have restNat := cardinality.nat with restFinite175    rw one at split176    have restZero : cardinality(A ∖ {a}) = 0177      have balance : cardinality(A ∖ {a}) + 1 = 0 + 1178        rw ← split179        compute180      exact add.right_cancel with balance181    have iff := cardinality.eq_zero_iff with restFinite182    have restEmpty := iff.forward with restZero183    have restored := insert.restore with member184    rw restEmpty at restored185    witness a186    rw ← restored187    ext z188    simp189  . intro singleton190    obtain ⟨x, shape⟩ := singleton191    rw shape192    exact cardinality.singleton at x193194theorem cardinality.equipotent (A B : Set)195  requires finite : Finite(A)196  requires equipotent : A ≃ B197  shows cardinality(A) = cardinality(B)198proof199  obtain ⟨f, bijective⟩ := equipotent200  exact cardinality.bijective with finite, bijective201202theorem cardinality.equipotent_of_eq (A B : Set)203  requires finiteA : Finite(A)204  requires finiteB : Finite(B)205  requires same : cardinality(A) = cardinality(B)206  shows A ≃ B207proof208  have countedA := HasCardinality.equipotent with (cardinality.correct with209    finiteA)210  have countedB := HasCardinality.equipotent with (cardinality.correct with211    finiteB)212  rw same at countedA213  have back := Equipotent.symmetric with countedB214  exact Equipotent.transitive with countedA, back215216theorem cardinality.eq_iff_equipotent (A B : Set)217  requires finiteA : Finite(A)218  requires finiteB : Finite(B)219  shows cardinality(A) = cardinality(B) ↔ A ≃ B220proof221  constructor222  . intro same223    exact cardinality.equipotent_of_eq with finiteA, finiteB, same224  . intro equipotent225    exact cardinality.equipotent with finiteA, equipotent226227-- A proper subset of a finite set is strictly smaller.228theorem cardinality.strict_of_ne (S T : Set)229  requires finite : Finite(T)230  requires subset : S ⊆ T231  requires different : S ≠ T232  shows cardinality(S) < cardinality(T)233proof234  have witness : ∃ a ∈ T, ¬a ∈ S235    by_contra none236    apply different237    apply Subset.antisymmetric with subset238    intros z hz239    by_contra outside240    apply none241    exact ⟨z, hz, outside⟩242  obtain ⟨a, member, fresh⟩ := witness243  exact cardinality.strict with finite, subset, member, fresh244245theorem cardinality.lt_iff_ne (S T : Set)246  requires finite : Finite(T)247  requires subset : S ⊆ T248  shows cardinality(S) < cardinality(T) ↔ S ≠ T249proof250  constructor251  . intro less252    intro equal253    rw equal at less254    have irreflexive := Less.irreflexive at cardinality(T)255    exact irreflexive with less256  . intro different257    exact cardinality.strict_of_ne with finite, subset, different258259theorem cardinality.eq_iff_subset_eq (S T : Set)260  requires finite : Finite(T)261  requires subset : S ⊆ T262  shows cardinality(S) = cardinality(T) ↔ S = T263proof264  constructor265  . intro same266    exact cardinality.eq_subset with finite, subset, same267  . intro equal268    rw equal269    rfl270271theorem cardinality.le_of_subset_natural (S : Set) (n : Nat)272  requires subset : S ⊆ n273  shows cardinality(S) ≤ n274proof275  have bound := cardinality.monotone with (Finite.natural at n), subset276  have same := cardinality.natural at n277  rw same at bound278  exact bound279280theorem cardinality.le_one_of_subset_singleton (S x : Set)281  requires subset : S ⊆ {x}282  shows cardinality(S) ≤ 1283proof284  have bound := cardinality.monotone with (Finite.singleton at x), subset285  have one := cardinality.singleton at x286  rw one at bound287  exact bound288289theorem cardinality.product_count (A B : Set)290  requires finiteA : Finite(A)291  requires finiteB : Finite(B)292  shows cardinality(A × B) = cardinality(A) * cardinality(B)293proof294  have countedA := cardinality.correct with finiteA295  have countedB := cardinality.correct with finiteB296  have product := HasCardinality.product with countedA, countedB297  exact cardinality.eq_of_has with product298299theorem cardinality.disjointSum_count (A B : Set)300  requires finiteA : Finite(A)301  requires finiteB : Finite(B)302  shows cardinality(A ⊎ B) = cardinality(A) + cardinality(B)303proof304  have countedA := cardinality.correct with finiteA305  have countedB := cardinality.correct with finiteB306  have sum := HasCardinality.disjointSum with countedA, countedB307  exact cardinality.eq_of_has with sum308309theorem powerset.count (A : Set)310  requires finite : Finite(A)311  shows cardinality(𝒫(A)) = 2 ^ cardinality(A)312proof313  have counted := cardinality.correct with finite314  have natA := cardinality.nat with finite315  have power := powerset.cardinality at A, cardinality(A) with counted316  exact cardinality.eq_of_has with power317318theorem cardinality.square (A : Set)319  requires finite : Finite(A)320  shows cardinality(A × A) = cardinality(A) * cardinality(A)321proof322  exact cardinality.product_count with finite, finite323324theorem cardinality.product_commutative (A B : Set)325  requires finiteA : Finite(A)326  requires finiteB : Finite(B)327  shows cardinality(A × B) = cardinality(B × A)328proof329  have left := cardinality.product_count with finiteA, finiteB330  have right := cardinality.product_count with finiteB, finiteA331  have natA := cardinality.nat with finiteA332  have natB := cardinality.nat with finiteB333  rw [left, right]334  ring335336theorem cardinality.subsets_count (A : Set) (k : Nat)337  requires finite : Finite(A)338  shows cardinality(subsetsOfSize(A, k)) = cardinality(A) choose k339proof340  exact combinations.count with finite341342theorem subsetsOfSize.finite (A : Set) (k : Nat)343  requires finite : Finite(A)344  shows Finite(subsetsOfSize(A, k))345proof346  have inside : subsetsOfSize(A, k) ⊆ 𝒫(A)347    intros S hS348    have parts := subsetsOfSize.membership.forward with hS349    exact parts.left350  exact Finite.subset with (Finite.powerset with finite), inside351