Grace/Cumulus/Cardinal/Finite.g17

Open in Workbench Download source

Imports

Function · Set.Ordinal · Nat

Declarations

Source

1-- Finite cardinality and equipotence2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.Finite8import Function9import Set.Ordinal10import Nat1112-- Cardinal comparison starts from set-valued bijections.  There is no13-- quotient or meta-level notion of cardinal behind these definitions.14predicate Equipotent (A B : Set) := ∃ f, BijectiveBetween(f, A, B)15notation infix 50 "≃" => Equipotent1617predicate HasCardinality (A n : Set) := Nat(n) ∧ A ≃ n18predicate Finite (A : Set) := ∃ n, HasCardinality(A, n)1920-- The unique graph carrying x to 0. Since 1 is the von Neumann singleton21-- {0}, this is the canonical bijection from {x} to 1.22def singletonEquiv (x : Set) : Set := {(x ↦ 0)}2324theorem one.membership (z : Set)25  shows z ∈ 1 ↔ z = 026proof27  have successorZero := next.natural at 028  rw successorZero29  simp [next.membership, nat.zero, set.empty]3031theorem singletonEquiv.membership (p x : Set)32  shows p ∈ singletonEquiv(x) ↔ p = (x ↦ 0)33proof34  simp [singletonEquiv, singleton.membership]3536theorem singletonEquiv.relation (x : Set)37  shows RelationBetween(singletonEquiv(x), {x}, 1)38proof39  intros p hp40  simp [singletonEquiv.membership] at hp41  rw hp42  apply product.pair43  exact singleton.self44  apply one.membership.backward45  rfl4647theorem singletonEquiv.functional (x : Set)48  shows Functional(singletonEquiv(x))49proof50  intros a b hab c hac51  unfold relates at hab52  simp [singletonEquiv.membership] at hab53  obtain (hax, hb0) := orderedPair.injective with hab54  unfold relates at hac55  simp [singletonEquiv.membership] at hac56  obtain (hax2, hc0) := orderedPair.injective with hac57  rw [hb0, hc0]58  rfl5960theorem singletonEquiv.function (x : Set)61  shows singletonEquiv(x) : {x} → 162proof63  constructor64  exact singletonEquiv.relation65  constructor66  exact singletonEquiv.functional67  intros a ha68  witness 069  constructor70  apply one.membership.backward71  rfl72  unfold relates73  apply singletonEquiv.membership.backward74  simp [singleton.membership] at ha75  rw ha76  rfl7778theorem singletonEquiv.injective (x : Set)79  shows InjectiveBetween(singletonEquiv(x), {x}, 1)80proof81  simp [InjectiveBetween, singletonEquiv.function]8283theorem singletonEquiv.surjective (x : Set)84  shows SurjectiveBetween(singletonEquiv(x), {x}, 1)85proof86  constructor87  exact singletonEquiv.function88  intros z hz89  simp [one.membership] at hz90  witness x91  constructor92  exact singleton.self93  unfold relates94  apply singletonEquiv.membership.backward95  rw hz96  rfl9798theorem singletonEquiv.bijective (x : Set)99  shows BijectiveBetween(singletonEquiv(x), {x}, 1)100proof101  refine ⟨singletonEquiv.injective at x, singletonEquiv.surjective at x⟩102103theorem Equipotent.singleton_one (x : Set)104  shows Equipotent({x}, 1)105proof106  witness singletonEquiv(x)107  exact singletonEquiv.bijective108109theorem Equipotent.reflexive (A : Set)110  shows Equipotent(A, A)111proof112  witness identity(A)113  exact identity.bijective114115theorem HasCardinality.empty_set116  shows HasCardinality(∅, 0)117proof118  constructor119  . exact Naturals.constructor.zero120  . rw nat.zero121    exact Equipotent.reflexive122123theorem Equipotent.symmetric (A B : Set)124  requires h : Equipotent(A, B)125  shows Equipotent(B, A)126proof127  simp [Equipotent, converse.bijective]128129theorem Equipotent.transitive (A B C : Set)130  requires hAB : Equipotent(A, B)131  requires hBC : Equipotent(B, C)132  shows Equipotent(A, C)133proof134  obtain (f, hf) := hAB135  obtain (g, hg) := hBC136  witness compose(g, f, A, B, C)137  exact compose.bijective with hf, hg138139theorem HasCardinality.natural (A n : Set)140  requires h : HasCardinality(A, n)141  shows Nat(n)142proof143  rcases h with (natural, equipotent)144  exact natural145146theorem HasCardinality.equipotent (A n : Set)147  requires h : HasCardinality(A, n)148  shows Equipotent(A, n)149proof150  rcases h with (natural, equipotent)151  exact equipotent152153theorem Finite.from_cardinality (A n : Set)154  requires h : HasCardinality(A, n)155  shows Finite(A)156proof157  witness n158  exact h159160theorem Finite.natural (n : Nat)161  shows Finite(n)162proof163  witness n164  refine ⟨assumption, Equipotent.reflexive at n⟩165166theorem Finite.enumeration (D : Set)167  requires finite : Finite(D)168  shows ∃ n, Nat(n) ∧ ∃ f, BijectiveBetween(f, n, D)169proof170  obtain ⟨n, natural, equivalent⟩ := finite171  obtain ⟨f, bijective⟩ := equivalent172  have inverse := converse.bijective with bijective173  refine ⟨n, natural, converse(f, D, n), inverse⟩174175theorem Finite.of_equipotent (A B : Set)176  requires finiteA : Finite(A)177  requires hAB : Equipotent(A, B)178  shows Finite(B)179proof180  obtain ⟨n, natural, hAn⟩ := finiteA181  witness n182  constructor183  exact natural184  have hBA := Equipotent.symmetric with hAB185  exact Equipotent.transitive with hBA, hAn186187theorem Finite.zero188  shows Finite(0)189proof190  simp [Finite.natural, Naturals.constructor.zero]191192theorem Finite.empty193  shows Finite(∅)194proof195  rw ← nat.zero196  exact Finite.zero197198theorem Finite.singleton (x : Set)199  shows Finite({x})200proof201  witness 1202  constructor203  have zeroNatural := Naturals.constructor.zero204  exact Naturals.constructor.succ with zeroNatural205  exact Equipotent.singleton_one206207-- A finite sequence of natural-valued function outputs has a common strict208-- bound.  This graph-level lemma is the bridge from cardinal finiteness to209-- number-theoretic boundedness.210lemma TotalBetween.bounded_step (f A a : Set, k b c : Nat)211  requires bounded : ∀ x ∈ k, ∀ y ∈ A, relates(f, x, y) → y ∈ succ(b)212  requires functional : Functional(f)213  requires hka : relates(f, k, a)214  requires aIn : a ∈ succ(c)215  requires lift : ∀ y ∈ succ(b), y ∈ succ(c)216  shows ∀ x ∈ succ(k), ∀ y ∈ A, relates(f, x, y) → y ∈ succ(c)217proof218  intros x hx y hyA hxy219  have xShape := membership.successor_forward{n := k} at x220  cases xShape with hxOld | hxCurrent221  . exact lift with y, (bounded with x, hxOld, y, hyA, hxy)222  . rw hxCurrent at hxy223    have unique := Functional.unique with functional, hxy, hka224    rwa unique225226lemma TotalBetween.natural_values_bounded (f A : Set, n : Nat)227  requires functional : Functional(f)228  requires naturalValues : ∀ y ∈ A, Nat(y)229  shows TotalBetween(f, n, A) → ∃ b, Nat(b) ∧ (∀ x ∈ n, ∀ y ∈ A, relates(f, x, y) → y ∈ succ(b))230proof231  induction n232  | zero =>233    intro total234    witness 0235    intros x hx236    exfalso237    simp [nat.zero, set.empty]238  | succ(k) using ih =>239    intro total240    have previousTotal := TotalBetween.predecessor with h_k, total241    obtain ⟨b, hbNat, bounded⟩ := ih with previousTotal242    have kMember := membership.self_successor with h_k243    obtain ⟨a, haA, hka⟩ := total with k, kMember244    have haNat := naturalValues with haA245    have haOrdinal := Ordinal.natural with haNat246    have hbOrdinal := Ordinal.natural with hbNat247    have comparison := Ordinal.trichotomy with haOrdinal, b, hbOrdinal248    cases comparison with haInB | hRest249    . have aIn : a ∈ succ(b) by simp250      have lift : ∀ y ∈ succ(b), y ∈ succ(b) by simp251      exact ⟨b, hbNat, (TotalBetween.bounded_step with bounded, functional, hka, aIn, lift)⟩252    . cases hRest with haEqB | hbInA253      . have aIn : a ∈ succ(b) by simp254        have lift : ∀ y ∈ succ(b), y ∈ succ(b) by simp255        exact ⟨b, hbNat, (TotalBetween.bounded_step with bounded, functional, hka, aIn, lift)⟩256      . have aIn := membership.self_successor with haNat257        have lift : ∀ y ∈ succ(b), y ∈ succ(a)258          intros y hy259          exact membership.successor_monotone with haNat, hbNat, hbInA, hy260        exact ⟨a, haNat, (TotalBetween.bounded_step with bounded, functional, hka, aIn, lift)⟩261262lemma Subset.omega_elements_natural (A : Set)263  requires hNatural : A ⊆ ℕ264  shows ∀ y ∈ A, Nat(y)265proof266  simp [Subset, omega.natural]267268theorem Finite.naturals_bounded (A : Set)269  requires hNatural : A ⊆ ℕ270  requires hFinite : Finite(A)271  shows ∃ b, Nat(b) ∧ (∀ y ∈ A, y ∈ succ(b))272proof273  obtain ⟨n, hnNat, f, hf⟩ := hFinite274  have inverse := converse.bijective with hf275  have surjective := Bijective.surjective with inverse276  have fn := Surjective.function with surjective277  have functional := FunctionBetween.functional with fn278  have total := FunctionBetween.total with fn279  have naturalValues := Subset.omega_elements_natural with hNatural280  obtain ⟨b, hbNat, bounded⟩ := TotalBetween.natural_values_bounded with hnNat, functional, naturalValues, total281  witness b282  intros y hyA283  rcases surjective with ⟨surjectiveFunction, onto⟩284  specialize onto with y, hyA285  obtain ⟨x, hxN, hxy⟩ := onto286  exact bounded with x, hxN, y, hyA, hxy287288-- A reusable public bridge from finite cardinality to Nat order:289-- no finite set of naturals can have an element strictly above every bound.290theorem infinite.of_unbounded_naturals (A : Set)291  requires hNatural : A ⊆ ℕ292  requires hUnbounded : ∀ n, Nat(n) → ∃ y ∈ A, n < y293  shows ¬Finite(A)294proof295  intro hFinite296  obtain ⟨b, hbNat, allBounded⟩ := Finite.naturals_bounded with hNatural, hFinite297  obtain ⟨y, hyA, hbLessY⟩ := hUnbounded with hbNat298  have naturalValues := Subset.omega_elements_natural with hNatural299  have hyNat := naturalValues with hyA300  have hbInY := membership.of_Less with hbNat, hyNat, hbLessY301  specialize allBounded with y, hyA302  have shape := membership.successor_forward{n := b} at y303  cases shape with hyInB | hyEqB304  . have hyOrdinal := Ordinal.natural at y with hyNat305    have transitive := Ordinal.transitive with hyOrdinal306    have bSubsetY := transitive with hbInY, y, hyInB307    exact membership.irreflexive with bSubsetY308  . rw hyEqB at hbInY309    exact membership.irreflexive with hbInY310311theorem omega.order_unbounded (n : Set)312  requires hn : Nat(n)313  shows ∃ y ∈ ℕ, n < y314proof315  witness succ(n)316  constructor317  . have successor := Naturals.constructor.succ at n with hn318    exact nat.omega.forward with successor319  . unfold Less320    have successor := Naturals.constructor.succ with hn321    exact LessEqual.reflexive with successor322323theorem omega.infinite324  shows ¬Finite(ℕ)325proof326  have natural := Subset.reflexive at ℕ327  have unbounded : ∀ n, Nat(n) → ∃ y ∈ ℕ, n < y by exact omega.order_unbounded328  exact infinite.of_unbounded_naturals with natural, unbounded329