Grace/Cumulus/Combinatorics/Pigeonhole.g17

Open in Workbench Download source

Imports

InclusionExclusion

Declarations

Source

1-- The pigeonhole principle for finite sets: an injection never shrinks a set,2-- a surjection never grows one, a function from a larger set into a smaller3-- one collides somewhere, and between finite sets of the same size injective,4-- surjective, and bijective coincide5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.Pigeonhole11import InclusionExclusion1213theorem Injective.apply_ne (f A B x y : Set)14  requires injective : InjectiveBetween(f, A, B)15  requires hx : x ∈ A16  requires hy : y ∈ A17  requires different : x ≠ y18  shows f(x) ≠ f(y)19proof20  intro same21  apply different22  exact Injective.apply_cancel with injective, hx, hy, same2324theorem Surjective.image_full (f A B : Set)25  requires surjective : SurjectiveBetween(f, A, B)26  shows functionImage(f, A, B) = B27proof28  have function := Surjective.function with surjective29  apply Subset.antisymmetric with (functionImage.subset at f, A, B)30  intros y hy31  obtain ⟨x, hx, related⟩ := surjective.right with y, hy32  have value := FunctionBetween.apply_value with function, hx, related33  apply functionImage.membership.backward34  refine ⟨hy, x, hx, ?_⟩35  symm36  exact value3738theorem Surjective.of_image_full (f A B : Set)39  requires function : f : A → B40  requires full : functionImage(f, A, B) = B41  shows SurjectiveBetween(f, A, B)42proof43  unfold SurjectiveBetween44  refine ⟨function, ?_⟩45  intros y hy46  rw ← full at hy47  obtain ⟨inB, x, hx, shape⟩ := functionImage.membership.forward with hy48  refine ⟨x, hx, ?_⟩49  rw shape50  exact FunctionBetween.relates_apply with function, hx5152theorem Injective.image_count (f A B : Set)53  requires injective : InjectiveBetween(f, A, B)54  requires finite : Finite(A)55  shows cardinality(functionImage(f, A, B)) = cardinality(A)56proof57  exact cardinality.injective_image with injective, (Subset.reflexive at A), finite5859theorem Injective.finite_domain (f A B : Set)60  requires injective : InjectiveBetween(f, A, B)61  requires finite : Finite(B)62  shows Finite(A)63proof64  have dominated := Dominated.of_injective with injective65  exact Finite.of_dominated with finite, dominated6667-- An injection never shrinks a finite set.68theorem Injective.cardinality_le (f A B : Set)69  requires injective : InjectiveBetween(f, A, B)70  requires finite : Finite(B)71  shows cardinality(A) ≤ cardinality(B)72proof73  have finiteA := Injective.finite_domain with injective, finite74  have image := Injective.image_count with injective, finiteA75  have bound := cardinality.monotone with76    finite, (functionImage.subset at f, A, B)77  rw image at bound78  exact bound7980theorem Dominated.cardinality_le (A B : Set)81  requires dominated : A ≼ B82  requires finite : Finite(B)83  shows cardinality(A) ≤ cardinality(B)84proof85  obtain ⟨f, injective⟩ := dominated86  exact Injective.cardinality_le with injective, finite8788theorem Surjective.finite_codomain (f A B : Set)89  requires surjective : SurjectiveBetween(f, A, B)90  requires finite : Finite(A)91  shows Finite(B)92proof93  have function := Surjective.function with surjective94  have full := Surjective.image_full with surjective95  have finiteImage := Finite.function_image with96    function, finite, (Subset.reflexive at A)97  rw full at finiteImage98  exact finiteImage99100-- A surjection never grows a finite set.101theorem Surjective.cardinality_ge (f A B : Set)102  requires surjective : SurjectiveBetween(f, A, B)103  requires finite : Finite(A)104  shows cardinality(B) ≤ cardinality(A)105proof106  have function := Surjective.function with surjective107  have full := Surjective.image_full with surjective108  have bound := cardinality.image_le with109    function, (Subset.reflexive at A), finite110  rw full at bound111  exact bound112113-- The pigeonhole principle: more pigeons than holes forces a shared hole.114theorem pigeonhole.not_injective (f A B : Set)115  requires function : f : A → B116  requires finite : Finite(B)117  requires more : cardinality(B) < cardinality(A)118  shows ¬InjectiveBetween(f, A, B)119proof120  intro injective121  have bound := Injective.cardinality_le with injective, finite122  have natA := cardinality.nat with (Injective.finite_domain with123    injective, finite)124  have natB := cardinality.nat with finite125  have strict := Less.transitive_LessEqual with more, bound126  exact Less.irreflexive at cardinality(B) with strict127128theorem pigeonhole.collision (f A B : Set)129  requires function : f : A → B130  requires finite : Finite(B)131  requires more : cardinality(B) < cardinality(A)132  shows ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ f(x) = f(y)133proof134  by_contra none135  have cancel : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → x = y136    intros x hx y hy same137    by_contra different138    apply none139    exact ⟨x, hx, y, hy, different, same⟩140  have injective := Injective.of_pointwise with function, cancel141  exact pigeonhole.not_injective with function, finite, more, injective142143theorem pigeonhole.successor (f : Set) (n : Nat)144  shows ¬InjectiveBetween(f, n + 1, n)145proof146  intro injective147  have bound := Injective.cardinality_le with injective, (Finite.natural at n)148  have one : n + 1 = succ(n) := add.right_one with *149  have sizeSucc := cardinality.natural at succ(n)150  have size := cardinality.natural at n151  rw one at bound152  rw [sizeSucc, size] at bound153  arith154155theorem pigeonhole.not_dominated (n : Nat)156  shows ¬(n + 1 ≼ n)157proof158  intro dominated159  obtain ⟨f, injective⟩ := dominated160  exact pigeonhole.successor at f, n with injective161162theorem pigeonhole.not_equipotent (n : Nat)163  shows ¬(n + 1 ≃ n)164proof165  intro equipotent166  have dominated := Dominated.of_equipotent with equipotent167  exact pigeonhole.not_dominated at n with dominated168169-- Two naturals are equipotent exactly when they are equal.170theorem natural.equipotent_iff (m n : Nat)171  shows m ≃ n ↔ m = n172proof173  constructor174  . intro equipotent175    have counted : HasCardinality(m, n) := ⟨assumption, equipotent⟩176    have size := cardinality.eq_of_has with counted177    have own := cardinality.natural at m178    rw own at size179    exact size180  . intro equal181    rw equal182    exact Equipotent.reflexive at n183184theorem natural.subset_of_le (m d : Nat)185  shows m ⊆ m + d186proof187  induction d188  | zero =>189    have shape : m + 0 = m by ring190    rw shape191    exact Subset.reflexive at m192  | k + 1 using ih =>193    have shape : m + (k + 1) = succ(m + k) by ring194    rw shape195    intros x hx196    have inside := ih with x, hx197    have sumNat : Nat(m + k) by typecheck198    exact membership.into_successor at x, m + k with inside199200theorem natural.subset_of_LessEqual (m n : Nat)201  requires le : m ≤ n202  shows m ⊆ n203proof204  obtain ⟨d, dNat, shape⟩ := le205  rw ← shape206  exact natural.subset_of_le at m, d207208theorem Dominated.of_cardinality_le (A B : Set)209  requires finiteA : Finite(A)210  requires finiteB : Finite(B)211  requires le : cardinality(A) ≤ cardinality(B)212  shows A ≼ B213proof214  have natA := cardinality.nat with finiteA215  have natB := cardinality.nat with finiteB216  have countedA := HasCardinality.equipotent with (cardinality.correct with217    finiteA)218  have countedB := HasCardinality.equipotent with (cardinality.correct with219    finiteB)220  have subset := natural.subset_of_LessEqual with le221  have first := Dominated.of_equipotent with countedA222  have second := Dominated.of_subset with subset223  have third := Dominated.of_equipotent with (Equipotent.symmetric with224    countedB)225  exact Dominated.transitive with first, (Dominated.transitive with second, third)226227theorem Dominated.iff_cardinality_le (A B : Set)228  requires finiteA : Finite(A)229  requires finiteB : Finite(B)230  shows A ≼ B ↔ cardinality(A) ≤ cardinality(B)231proof232  constructor233  . intro dominated234    exact Dominated.cardinality_le with dominated, finiteB235  . intro le236    exact Dominated.of_cardinality_le with finiteA, finiteB, le237238-- Between finite sets of the same size, a surjection is injective.239theorem Finite.injective_of_surjective (f A B : Set)240  requires surjective : SurjectiveBetween(f, A, B)241  requires finite : Finite(A)242  requires same : cardinality(A) = cardinality(B)243  shows InjectiveBetween(f, A, B)244proof245  have function := Surjective.function with surjective246  have full := Surjective.image_full with surjective247  have whole := Subset.reflexive at A248  apply Injective.of_pointwise with function249  intros x hx y hy equal250  have imageCount : cardinality(functionImage(f, A, B)) = cardinality(A)251    rw [full, same]252    rfl253  exact cardinality.injective_of_image with function, whole, finite, imageCount, hx, hy, equal254255-- Between finite sets of the same size, an injection is surjective.256theorem Finite.surjective_of_injective (f A B : Set)257  requires injective : InjectiveBetween(f, A, B)258  requires finite : Finite(B)259  requires same : cardinality(A) = cardinality(B)260  shows SurjectiveBetween(f, A, B)261proof262  have function := Injective.function with injective263  have finiteA := Injective.finite_domain with injective, finite264  have image := Injective.image_count with injective, finiteA265  rw same at image266  have full := cardinality.eq_subset with267    finite, (functionImage.subset at f, A, B), image268  exact Surjective.of_image_full with function, full269270theorem Finite.bijective_of_injective (f A B : Set)271  requires injective : InjectiveBetween(f, A, B)272  requires finite : Finite(B)273  requires same : cardinality(A) = cardinality(B)274  shows BijectiveBetween(f, A, B)275proof276  have surjective := Finite.surjective_of_injective with injective, finite, same277  exact ⟨injective, surjective⟩278279theorem Finite.bijective_of_surjective (f A B : Set)280  requires surjective : SurjectiveBetween(f, A, B)281  requires finite : Finite(A)282  requires same : cardinality(A) = cardinality(B)283  shows BijectiveBetween(f, A, B)284proof285  have injective := Finite.injective_of_surjective with surjective, finite, same286  exact ⟨injective, surjective⟩287288theorem Finite.injective_iff_surjective (f A B : Set)289  requires function : f : A → B290  requires finiteA : Finite(A)291  requires finiteB : Finite(B)292  requires same : cardinality(A) = cardinality(B)293  shows InjectiveBetween(f, A, B) ↔ SurjectiveBetween(f, A, B)294proof295  constructor296  . intro injective297    exact Finite.surjective_of_injective with injective, finiteB, same298  . intro surjective299    exact Finite.injective_of_surjective with surjective, finiteA, same300301theorem Finite.injective_iff_bijective (f A B : Set)302  requires finiteB : Finite(B)303  requires same : cardinality(A) = cardinality(B)304  shows InjectiveBetween(f, A, B) ↔ BijectiveBetween(f, A, B)305proof306  constructor307  . intro injective308    exact Finite.bijective_of_injective with injective, finiteB, same309  . intro bijective310    exact Bijective.injective with bijective311312theorem Finite.surjective_iff_bijective (f A B : Set)313  requires finiteA : Finite(A)314  requires same : cardinality(A) = cardinality(B)315  shows SurjectiveBetween(f, A, B) ↔ BijectiveBetween(f, A, B)316proof317  constructor318  . intro surjective319    exact Finite.bijective_of_surjective with surjective, finiteA, same320  . intro bijective321    exact Bijective.surjective with bijective322323-- Self-maps of a finite set.324theorem Finite.self_injective_bijective (f A : Set)325  requires injective : InjectiveBetween(f, A, A)326  requires finite : Finite(A)327  shows BijectiveBetween(f, A, A)328proof329  have same : cardinality(A) = cardinality(A) by rfl330  exact Finite.bijective_of_injective with injective, finite, same331332theorem Finite.self_surjective_bijective (f A : Set)333  requires surjective : SurjectiveBetween(f, A, A)334  requires finite : Finite(A)335  shows BijectiveBetween(f, A, A)336proof337  have same : cardinality(A) = cardinality(A) by rfl338  exact Finite.bijective_of_surjective with surjective, finite, same339340-- A collision shrinks the image.341theorem pigeonhole.image_strict (f A B x y : Set)342  requires function : f : A → B343  requires finite : Finite(A)344  requires hx : x ∈ A345  requires hy : y ∈ A346  requires different : x ≠ y347  requires same : f(x) = f(y)348  shows cardinality(functionImage(f, A, B)) < cardinality(A)349proof350  have whole := Subset.reflexive at A351  have bound := cardinality.image_le with function, whole, finite352  have natImage := cardinality.nat with (Finite.function_image with353    function, finite, whole)354  have natA := cardinality.nat with finite355  have notFull : cardinality(functionImage(f, A, B)) ≠ cardinality(A)356    intro full357    apply different358    exact cardinality.injective_of_image with function, whole, finite, full, hx, hy, same359  have alternatives := Less.trichotomy at cardinality(functionImage(f, A, B)), cardinality(A) with natImage, natA360  rcases alternatives with less | equal | greater361  . exact less362  . exfalso363    exact notFull with equal364  . exfalso365    have strict := Less.transitive_LessEqual with greater, bound366    exact Less.irreflexive at cardinality(A) with strict367