Grace/Cumulus/Cardinal/Pigeonhole.g17

Open in Workbench Download source

Imports

NaturalSum

Declarations

Source

1-- Cardinality is monotone on finite sets, strictly so for proper subsets,2-- an image is no larger than its domain, and a function whose image is as3-- large as its finite domain is injective4-- 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.Pigeonhole10import NaturalSum1112theorem cardinality.nat (A : Set)13  requires finite : Finite(A)14  shows Nat(cardinality(A))15proof16  exact HasCardinality.natural with (cardinality.correct with finite)1718theorem cardinality.monotone (S T : Set)19  requires finite : Finite(T)20  requires subset : S ⊆ T21  shows cardinality(S) ≤ cardinality(T)22proof23  have finiteS := Finite.subset with finite, subset24  have restSubset := difference.subset_left at T, S25  have finiteRest := Finite.subset with finite, restSubset26  have disjoint := Disjoint.symmetric with (difference.disjoint at T, S)27  have restored : S ∪ (T ∖ S) = T28    ext z29    simp30  have count := cardinality.union_disjoint with finiteS, finiteRest, disjoint31  rw restored at count32  have natS := cardinality.nat with finiteS33  have natRest := cardinality.nat with finiteRest34  rw count35  arith3637theorem cardinality.strict (S T a : Set)38  requires finite : Finite(T)39  requires subset : S ⊆ T40  requires member : a ∈ T41  requires fresh : ¬a ∈ S42  shows cardinality(S) < cardinality(T)43proof44  have finiteS := Finite.subset with finite, subset45  have inserted : insert(a, S) ⊆ T46    intros z hz47    have split := insert.membership.forward with hz48    cases split with same | inS49    . rw same50      exact member51    . exact subset with z, inS52  have count := cardinality.insert with finiteS, fresh53  have mono := cardinality.monotone with finite, inserted54  rw count at mono55  have natS := cardinality.nat with finiteS56  have natT := cardinality.nat with finite57  arith5859theorem cardinality.eq_subset (S T : Set)60  requires finite : Finite(T)61  requires subset : S ⊆ T62  requires same : cardinality(S) = cardinality(T)63  shows S = T64proof65  apply Subset.antisymmetric with subset66  intros z hz67  by_contra outside68  have strict := cardinality.strict with finite, subset, hz, outside69  have natS := cardinality.nat with (Finite.subset with finite, subset)70  have natT := cardinality.nat with finite71  rw same at strict72  arith7374theorem cardinality.insert_le (A a : Set)75  requires finite : Finite(A)76  shows cardinality(insert(a, A)) ≤ succ(cardinality(A))77proof78  have natA := cardinality.nat with finite79  have alternatives : a ∈ A ∨ ¬a ∈ A by tauto80  cases alternatives with inside | fresh81  . have same : insert(a, A) = A82      ext z83      constructor84      . intro hz85        have split := insert.membership.forward with hz86        cases split with equal | inA87        . rw equal88          exact inside89        . exact inA90      . intro hz91        apply insert.membership.backward92        right93        exact hz94    rw same95    arith96  . have count := cardinality.insert with finite, fresh97    rw count98    arith99100theorem cardinality.image_bounded (f A B : Set) (k : Nat)101  requires function : f : A → B102  shows ∀ S, S ⊆ A → HasCardinality(S, k) → cardinality(functionImage(f, S, B)) ≤ k103proof104  induction k105  | zero =>106    intros S subset counted107    have empty := HasCardinality.empty_of_zero at S with counted108    rw [empty, functionImage.empty, ← nat.zero]109    have zero := cardinality.natural at 0110    rw zero111    arith112  | succ(j) using ih =>113    intros S subset counted114    obtain ⟨x, hx⟩ := HasCardinality.exists_member with counted115    have finite := Finite.from_cardinality with counted116    have count := cardinality.eq_of_has with counted117    have removed := cardinality.remove with finite, hx118    have restSubset := difference.subset_left at S, {x}119    have smallerFinite := Finite.subset with finite, restSubset120    have smallerNat := cardinality.nat with smallerFinite121    have smallerCount : cardinality(S ∖ {x}) = j122      rw count at removed123      have forward : cardinality(S ∖ {x}) ≤ j by arith124      have backward : j ≤ cardinality(S ∖ {x}) by arith125      exact LessEqual.antisymmetric with forward, backward126    have smallerHas : HasCardinality(S ∖ {x}, j)127      rw ← smallerCount128      exact cardinality.correct with smallerFinite129    have smallerSubset := Subset.transitive with restSubset, subset130    have bound := ih with smallerSubset, smallerHas131    have xInA := subset with x, hx132    have image := functionImage.insert at f, A, B, x, S ∖ {x} with function, xInA133    have restored := insert.restore with hx134    rw restored at image135    rw image136    have finiteImage := Finite.function_image with function, smallerFinite, smallerSubset137    have step := cardinality.insert_le at functionImage(f, S ∖ {x}, B), f(x) with finiteImage138    have natImage := cardinality.nat with finiteImage139    arith140141theorem cardinality.image_le (f A B S : Set)142  requires function : f : A → B143  requires subset : S ⊆ A144  requires finite : Finite(S)145  shows cardinality(functionImage(f, S, B)) ≤ cardinality(S)146proof147  have counted := cardinality.correct with finite148  have natS := cardinality.nat with finite149  have all := cardinality.image_bounded with function150  exact all with subset, counted151152-- A function whose image is as large as its finite domain is injective.153theorem cardinality.injective_of_image (f A B S x y : Set)154  requires function : f : A → B155  requires subset : S ⊆ A156  requires finite : Finite(S)157  requires full : cardinality(functionImage(f, S, B)) = cardinality(S)158  requires hx : x ∈ S159  requires hy : y ∈ S160  requires same : f(x) = f(y)161  shows x = y162proof163  by_contra different164  have restSubset := difference.subset_left at S, {x}165  have smallerFinite := Finite.subset with finite, restSubset166  have smallerSubset := Subset.transitive with restSubset, subset167  have yRest : y ∈ S ∖ {x}168    apply difference.singleton_membership.backward169    constructor170    . exact hy171    . intro equal172      apply different173      symm174      exact equal175  have inclusion : functionImage(f, S, B) ⊆ functionImage(f, S ∖ {x}, B)176    intros z hz177    obtain ⟨zIn, w, hw, shape⟩ := functionImage.membership.forward with hz178    apply functionImage.membership.backward179    constructor180    . exact zIn181    . have alternatives : w = x ∨ w ≠ x182        tauto183      cases alternatives with wx | wnx184      . witness y185        constructor186        . exact yRest187        . rw [shape, wx, same]188          rfl189      . refine ⟨w, (difference.singleton_membership.backward with ⟨hw, wnx⟩), shape⟩190  have finiteImage := Finite.function_image with function, finite, subset191  have finiteSmallImage := Finite.function_image with function, smallerFinite, smallerSubset192  have mono := cardinality.monotone with finiteSmallImage, inclusion193  have le := cardinality.image_le with function, smallerSubset, smallerFinite194  have removed := cardinality.remove with finite, hx195  have natImage := cardinality.nat with finiteImage196  have natSmallImage := cardinality.nat with finiteSmallImage197  have natSmaller := cardinality.nat with smallerFinite198  have natS := cardinality.nat with finite199  arith200