Grace/Cumulus/Combinatorics/RamseyPigeonhole.g17

Open in Workbench Download source

Imports

Partitions · Cardinal.Dominance

Declarations

Source

1-- Infinite sets survive removing a point and pass through injections,2-- subsets of a given size under inclusion, insertion, and removal, and the3-- infinite pigeonhole principle: a map from an infinite set to a finite set4-- has an infinite fibre5-- 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.RamseyPigeonhole11import Partitions12import Cardinal.Dominance1314-- Infinite sets1516theorem Infinite.nonempty (A : Set)17  requires infinite : Infinite(A)18  shows Nonempty(A)19proof20  by_contra none21  have empty : A = ∅22    by_contra different23    exact none with (Nonempty.of_ne_empty with different)24  unfold Infinite at infinite25  apply infinite26  rw empty27  exact Finite.empty2829theorem Infinite.remove (A a : Set)30  requires infinite : Infinite(A)31  shows Infinite(A ∖ {a})32proof33  unfold Infinite34  intro finite35  unfold Infinite at infinite36  apply infinite37  have inserted := Finite.insert at A ∖ {a}, a with finite38  have covered : A ⊆ insert(a, A ∖ {a}) by simp39  exact Finite.subset with inserted, covered4041theorem Infinite.of_equipotent (A B : Set)42  requires infinite : Infinite(A)43  requires equipotent : A ≃ B44  shows Infinite(B)45proof46  unfold Infinite47  intro finite48  unfold Infinite at infinite49  apply infinite50  exact Finite.of_equipotent with finite, (Equipotent.symmetric with equipotent)5152theorem Infinite.injective_image (f A B : Set)53  requires injective : InjectiveBetween(f, A, B)54  requires infinite : Infinite(A)55  shows Infinite(functionImage(f, A, B))56proof57  exact Infinite.of_equipotent with infinite, (Equipotent.image with injective)5859-- Subsets of a given size6061theorem subsetsOfSize.subset (T A k : Set)62  requires member : T ∈ subsetsOfSize(A, k)63  shows T ⊆ A64proof65  have parts := subsetsOfSize.membership.forward with member66  exact powerset.membership_iff.forward with parts.left6768theorem subsetsOfSize.counted (T A k : Set)69  requires member : T ∈ subsetsOfSize(A, k)70  shows HasCardinality(T, k)71proof72  have parts := subsetsOfSize.membership.forward with member73  exact parts.right7475theorem subsetsOfSize.of_subset (T A k : Set)76  requires subset : T ⊆ A77  requires counted : HasCardinality(T, k)78  shows T ∈ subsetsOfSize(A, k)79proof80  apply subsetsOfSize.membership.backward81  exact ⟨powerset.membership_iff.backward with subset, counted⟩8283theorem subsetsOfSize.monotone (A B k : Set)84  requires subset : A ⊆ B85  shows subsetsOfSize(A, k) ⊆ subsetsOfSize(B, k)86proof87  intros T hT88  have inA := subsetsOfSize.subset with hT89  have counted := subsetsOfSize.counted with hT90  have inB := Subset.transitive with inA, subset91  exact subsetsOfSize.of_subset with inB, counted9293theorem subsetsOfSize.member_of_subset (T A B k : Set)94  requires subset : A ⊆ B95  requires member : T ∈ subsetsOfSize(A, k)96  shows T ∈ subsetsOfSize(B, k)97proof98  have inA := subsetsOfSize.subset with member99  have counted := subsetsOfSize.counted with member100  have inB := Subset.transitive with inA, subset101  exact subsetsOfSize.of_subset with inB, counted102103-- Adjoining a fresh point of A to an n-subset of A gives an (n + 1)-subset.104theorem subsetsOfSize.insert_member (T A a : Set) (n : Nat)105  requires member : T ∈ subsetsOfSize(A, n)106  requires ha : a ∈ A107  requires fresh : ¬a ∈ T108  shows insert(a, T) ∈ subsetsOfSize(A, n + 1)109proof110  have subset := subsetsOfSize.subset with member111  have counted := subsetsOfSize.counted with member112  have one : n + 1 = succ(n) := add.right_one with *113  rw one114  have inserted : insert(a, T) ⊆ A115    intros x hx116    have split := insert.membership.forward with hx117    cases split with same | inT118    . rw same119      exact ha120    . exact subset with x, inT121  have insertedCount := HasCardinality.insert_fresh with counted, fresh122  exact subsetsOfSize.of_subset with inserted, insertedCount123124-- Removing a point of an (n + 1)-subset leaves an n-subset.125theorem subsetsOfSize.remove_member (U A a : Set) (n : Nat)126  requires member : U ∈ subsetsOfSize(A, n + 1)127  requires ha : a ∈ U128  shows U ∖ {a} ∈ subsetsOfSize(A, n)129proof130  have subset := subsetsOfSize.subset with member131  have counted := subsetsOfSize.counted with member132  have one : n + 1 = succ(n) := add.right_one with *133  rw one at counted134  have removed : U ∖ {a} ⊆ A :=135    Subset.transitive with (difference.subset_left at U, {a}), subset136  have removedCount := HasCardinality.remove with counted, ha137  exact subsetsOfSize.of_subset with removed, removedCount138139theorem subsetsOfSize.exists_member (U A : Set) (n : Nat)140  requires member : U ∈ subsetsOfSize(A, n + 1)141  shows ∃ u, u ∈ U142proof143  have counted := subsetsOfSize.counted with member144  have one : n + 1 = succ(n) := add.right_one with *145  rw one at counted146  exact HasCardinality.exists_member with counted147148-- The infinite pigeonhole principle149150-- The fibre of g over a point of the codomain, as a map into the subsets of151-- the domain.152defgraph fiberOf (g A K : Set) (c ∈ K) : 𝒫(A) :=153  functionPreimage(g, A, {c})154proof155  have subset := functionPreimage.subset at g, A, {c}156  exact powerset.membership_iff.backward with subset157158theorem pigeonhole.infinite_fiber (g A K : Set)159  requires function : g : A → K160  requires infinite : Infinite(A)161  requires finite : Finite(K)162  shows ∃ c ∈ K, Infinite(functionPreimage(g, A, {c}))163proof164  by_contra none165  have graph := fiberOf.function at g, A, K166  have fibresFinite : ∀ F ∈ functionImage(fiberOf(g, A, K), K, 𝒫(A)),167      Finite(F)168    intros F hF169    have parts := functionImage.membership.forward with hF170    obtain ⟨c, hc, shape⟩ := parts.right171    have value := fiberOf.value at g, A, K, c with hc172    rw [shape, value]173    by_contra notFinite174    apply none175    exact ⟨c, hc, notFinite⟩176  have familyFinite := Finite.function_image with177    graph, finite, (Subset.reflexive at K)178  have unionFinite := Finite.big_union with familyFinite, fibresFinite179  have covered : A ⊆ ⋃(functionImage(fiberOf(g, A, K), K, 𝒫(A)))180    intros x hx181    have valueK := FunctionBetween.apply_closed with function, hx182    have inFibre : x ∈ functionPreimage(g, A, {g(x)}) :=183      functionPreimage.point_membership.backward with ⟨hx, rfl⟩184    have value := fiberOf.value at g, A, K, g(x) with valueK185    have fibreIn := functionImage.value with graph, valueK186    rw value at fibreIn187    exact union.contains with fibreIn, inFibre188  unfold Infinite at infinite189  apply infinite190  exact Finite.subset with unionFinite, covered191