Grace/Cumulus/Geometry/Absorption/CountableUnion.g17

Open in Workbench Download source

Imports

Cardinal.CountableClosure · Cardinal.Infinite · Set.ChoiceFunctions

Declarations

Source

1-- Countable unions: a countable family of countable sets has a countable2-- union, coded through choice functions and the pairing of ℕ × ℕ3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Absorption.CountableUnion9import Cardinal.CountableClosure10import Cardinal.Infinite11import Set.ChoiceFunctions1213theorem Countable.of_injection (f A B : Set)14  requires injective : InjectiveBetween(f, A, B)15  requires countable : Countable(B)16  shows Countable(A)17proof18  obtain ⟨g, code⟩ := countable19  have composite := compose.injective with injective, code20  exact ⟨compose(g, f, A, B, ℕ), composite⟩2122theorem Countable.of_finite (A : Set)23  requires finite : Finite(A)24  shows Countable(A)25proof26  obtain ⟨n, natural, equivalent⟩ := finite27  obtain ⟨f, bijective⟩ := equivalent28  have injective := Bijective.injective with bijective29  have function := Injective.function with injective30  have values : ∀ x ∈ A, f(x) ∈ ℕ31    intros x hx32    have valueIn := FunctionBetween.apply_closed with function, hx33    have typed := natural.member at n with f(x), valueIn34    exact nat.omega.forward with typed35  have widened := FunctionBetween.codomain_of_values with function, values36  have cancel : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → x = y37    intros x hx y hy same38    exact Injective.apply_cancel with injective, hx, hy, same39  have intoNaturals := Injective.of_pointwise with widened, cancel40  exact ⟨f, intoNaturals⟩4142theorem Countable.image (f A B : Set)43  requires function : f : A → B44  requires countable : Countable(A)45  shows Countable(functionImage(f, A, B))46proof47  have surjection := functionImage.surjective with function48  exact Countable.of_surjection with countable, surjection4950theorem Finite.preimage (f A B Y : Set)51  requires injective : InjectiveBetween(f, A, B)52  requires finite : Finite(Y)53  shows Finite(functionPreimage(f, A, Y))54proof55  have function := Injective.function with injective56  have subset := functionPreimage.subset at f, A, Y57  have restricted := restrict.injective with injective, subset58  have values : ∀ x ∈ functionPreimage(f, A, Y),59      restrict(f, functionPreimage(f, A, Y))(x) ∈ Y60    intros x hx61    have inY := functionPreimage.membership.forward with hx62    have value := restrict.domain_apply with function, subset, hx63    rw value64    exact inY.right65  have restrictedFunction := Injective.function with restricted66  have intoY := FunctionBetween.codomain_of_values67    with restrictedFunction, values68  have cancel : ∀ x ∈ functionPreimage(f, A, Y),69      ∀ y ∈ functionPreimage(f, A, Y),70      restrict(f, functionPreimage(f, A, Y))(x) =71        restrict(f, functionPreimage(f, A, Y))(y) → x = y72    intros x hx y hy same73    exact Injective.apply_cancel with restricted, hx, hy, same74  have intoYInjective := Injective.of_pointwise with intoY, cancel75  have dominated : functionPreimage(f, A, Y) ≼ Y :=76    Dominated.of_injective with intoYInjective77  exact Finite.of_dominated with finite, dominated7879-- The injections of a set into ℕ: for A ⊆ X they are subsets of X × ℕ,80-- so a choice function on the subsets of 𝒫(X × ℕ) picks one for every81-- countable A ⊆ X.82def naturalInjections (A : Set) : Set :=83  { g ∈ 𝒫(A × ℕ) | InjectiveBetween(g, A, ℕ) }8485theorem naturalInjections.nonempty (A : Set)86  requires countable : Countable(A)87  shows Nonempty(naturalInjections(A))88proof89  obtain ⟨g, injective⟩ := countable90  have function := Injective.function with injective91  have relation := FunctionBetween.relation with function92  unfold RelationBetween at relation93  have inPower := powerset.membership_iff.backward with relation94  witness g95  apply naturalInjections.membership.backward96  exact ⟨inPower, injective⟩9798theorem naturalInjections.subset (A X : Set)99  requires subset : A ⊆ X100  shows naturalInjections(A) ⊆ 𝒫(X × ℕ)101proof102  intros g hg103  have data := naturalInjections.membership.forward with hg104  have same := Subset.reflexive at ℕ105  have pairs : A × ℕ ⊆ X × ℕ := product.monotone with subset, same106  have wider := powerset.monotone with pairs107  exact wider with g, data.left108109-- The injection of A into ℕ that the choice function c picks.110def naturalCode (c A : Set) : Set := c(naturalInjections(A))111112theorem naturalCode.injective (c A X : Set)113  requires choice : SubsetChoice(c, 𝒫(X × ℕ))114  requires subset : A ⊆ X115  requires countable : Countable(A)116  shows InjectiveBetween(naturalCode(c, A), A, ℕ)117proof118  have nonempty := naturalInjections.nonempty with countable119  have bounded := naturalInjections.subset with subset120  have member := SubsetChoice.member with choice, bounded, nonempty121  have data := naturalInjections.membership.forward with member122  unfold naturalCode123  exact data.right124125-- The members of the family containing a point of the union, and the126-- one that a choice function d on the subsets of the family picks.127def containers (S x : Set) : Set := { A ∈ S | x ∈ A }128def container (d S x : Set) : Set := d(containers(S, x))129130theorem containers.subset (S x : Set)131  shows containers(S, x) ⊆ S132proof133  intros A hA134  have data := containers.membership.forward with hA135  exact data.left136137theorem container.graph (d S x : Set)138  shows container(d, S, x) = d(containers(S, x))139proof140  simp [container]141142theorem container.member (d S x : Set)143  requires choice : SubsetChoice(d, S)144  requires hx : x ∈ ⋃(S)145  shows container(d, S, x) ∈ S ∧ x ∈ container(d, S, x)146proof147  obtain ⟨A, hA, inA⟩ := union.membership.forward with hx148  have inContainers := containers.membership.backward at S, x, A with ⟨hA, inA⟩149  have nonempty : Nonempty(containers(S, x)) := ⟨A, inContainers⟩150  have bounded := containers.subset at S, x151  have chosen := SubsetChoice.member with choice, bounded, nonempty152  rw container.graph153  exact containers.membership.forward with chosen154155-- The code of a point of the union: the code of its container under an156-- injection g of the family into ℕ, paired with its code inside the157-- container under the injection that c picks.158defgraph unionCode (S c d g : Set) (x ∈ ⋃(S)) : ℕ × ℕ :=159  (g(container(d, S, x)), naturalCode(c, container(d, S, x))(x))160requires choiceC : SubsetChoice(c, 𝒫(⋃(S) × ℕ))161requires choiceD : SubsetChoice(d, S)162requires code : InjectiveBetween(g, S, ℕ)163requires members : ∀ A ∈ S, Countable(A)164proof165  obtain ⟨containerIn, xIn⟩ := container.member with choiceD, member166  have outer := Injective.function with code167  have bounded := union.subset_of_member with containerIn168  have countable := members with container(d, S, x), containerIn169  have innerInjective := naturalCode.injective with choiceC, bounded, countable170  have inner := Injective.function with innerInjective171  have first := FunctionBetween.apply_closed with outer, containerIn172  have second := FunctionBetween.apply_closed with inner, xIn173  exact product.pair with first, second174175theorem unionCode.injective (S c d g : Set)176  requires choiceC : SubsetChoice(c, 𝒫(⋃(S) × ℕ))177  requires choiceD : SubsetChoice(d, S)178  requires code : InjectiveBetween(g, S, ℕ)179  requires members : ∀ A ∈ S, Countable(A)180  shows InjectiveBetween(unionCode(S, c, d, g), ⋃(S), ℕ × ℕ)181proof182  have function := unionCode.function with choiceC, choiceD, code, members183  apply Injective.of_pointwise with function184  intros x hx y hy same185  have valueX := unionCode.value with choiceC, choiceD, code, members, hx186  have valueY := unionCode.value with choiceC, choiceD, code, members, hy187  rw [valueX, valueY] at same188  obtain ⟨sameContainerCode, sameCode⟩ := orderedPair.injective with same189  obtain ⟨containerXIn, xIn⟩ := container.member with choiceD, hx190  obtain ⟨containerYIn, yIn⟩ := container.member with choiceD, hy191  have sameContainer := Injective.apply_cancel with192    code, containerXIn, containerYIn, sameContainerCode193  rw ← sameContainer at sameCode194  rw ← sameContainer at yIn195  have bounded := union.subset_of_member with containerXIn196  have countable := members with container(d, S, x), containerXIn197  have inner := naturalCode.injective with choiceC, bounded, countable198  exact Injective.apply_cancel with inner, xIn, yIn, sameCode199200-- A countable union of countable sets is countable: an injection of the201-- family into ℕ and two choice functions code every point of the union.202theorem Countable.union (S : Set)203  requires countable : Countable(S)204  requires members : ∀ A ∈ S, Countable(A)205  shows Countable(⋃(S))206proof207  obtain ⟨g, code⟩ := countable208  obtain ⟨c, choiceC⟩ := SubsetChoice.exists at 𝒫(⋃(S) × ℕ)209  obtain ⟨d, choiceD⟩ := SubsetChoice.exists at S210  have injective := unionCode.injective with choiceC, choiceD, code, members211  have pairs : Countable(ℕ × ℕ) :=212    ⟨naturalPairing, naturalPairing.injective⟩213  exact Countable.of_injection with injective, pairs214215theorem Countable.union2 (A B : Set)216  requires countableA : Countable(A)217  requires countableB : Countable(B)218  shows Countable(A ∪ B)219proof220  have singletonFinite := Finite.singleton at B221  have insertFinite := Finite.insert at {B}, A with singletonFinite222  have same : insert(A, {B}) = {A, B}223    ext y224    simp225  rw same at insertFinite226  have countablePair := Countable.of_finite with insertFinite227  have members : ∀ C ∈ {A, B}, Countable(C)228    intros C hC229    have cases : C = A ∨ C = B230      simp at hC231      exact hC232    cases cases with isA | isB233    . rw isA234      exact countableA235    . rw isB236      exact countableB237  have union := Countable.union with countablePair, members238  rw union.pair at union239  exact union240241-- The union of a countable family indexed by a function.242theorem Countable.indexed_union (F I X : Set)243  requires function : F : I → 𝒫(X)244  requires countable : Countable(I)245  requires members : ∀ i ∈ I, Countable(F(i))246  shows Countable(⋃(functionImage(F, I, 𝒫(X))))247proof248  have familyCountable := Countable.image with function, countable249  have each : ∀ A ∈ functionImage(F, I, 𝒫(X)), Countable(A)250    intros A hA251    obtain ⟨bounded, i, hi, shape⟩ :=252      functionImage.membership.forward with hA253    rw shape254    exact members with i, hi255  exact Countable.union with familyCountable, each256