Finite Exhaustions

This file defines a structure called FiniteExhaustion which represents an exhaustion of a countable set by an increasing sequence of finite sets. Given a countable set s, FiniteExhaustion.choice s is a choice of a finite exhaustion.

structure Set.FiniteExhaustion {α : Type u_1} (s : Set α) : Type u_1

A FiniteExhaustion of a set s is a monotonically increasing sequence of finite sets such that their union is s.

• toFun : ℕ → Set α

  The underlying sequence of a FiniteExhaustion.

• finite' (n : ℕ) : Finite ↑(self.toFun n)

  Every set in a FiniteExhaustion is finite.

• subset_succ' (n : ℕ) : self.toFun n ⊆ self.toFun (n + 1)

  The sequence of sets in a FiniteExhaustion are monotonically increasing.

• iUnion_eq' : ⋃ (n : ℕ), self.toFun n = s

  The union of all sets in a FiniteExhaustion equals s

instance Set.FiniteExhaustion.instFunLikeNat {α : Type u_1} {s : Set α} : FunLike s.FiniteExhaustion ℕ (Set α)

Equations

• Set.FiniteExhaustion.instFunLikeNat = { coe := Set.FiniteExhaustion.toFun, coe_injective' := ⋯ }

instance Set.FiniteExhaustion.instRelHomClassNatLeSubset {α : Type u_1} {s : Set α} : RelHomClass s.FiniteExhaustion LE.le Subset

instance Set.FiniteExhaustion.instFiniteElemCoeNat {α : Type u_1} {s : Set α} {K : s.FiniteExhaustion} {n : ℕ} : Finite ↑(K n)

@[simp]

theorem Set.FiniteExhaustion.toFun_eq_coe {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) : K.toFun = ⇑K

theorem Set.FiniteExhaustion.finite {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) (n : ℕ) : (K n).Finite

theorem Set.FiniteExhaustion.subset_succ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) (n : ℕ) : K n ⊆ K (n + 1)

theorem Set.FiniteExhaustion.mono {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) {m n : ℕ} (h : m ≤ n) : K m ⊆ K n

@[simp]

theorem Set.FiniteExhaustion.iUnion_eq {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) : ⋃ (n : ℕ), K n = s

noncomputable def Set.Countable.finiteExhaustion {α : Type u_1} {s : Set α} (hs : s.Countable) : s.FiniteExhaustion

A choice of a FiniteExhaustion for a countable set s.

Equations

• hs.finiteExhaustion = Classical.choice ⋯

theorem Set.FiniteExhaustion.Set.nonempty_finiteExhaustion_iff {α : Type u_1} {s : Set α} : Nonempty s.FiniteExhaustion ↔ s.Countable

def Set.FiniteExhaustion.prod {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) {β : Type u_2} {t : Set β} (K' : t.FiniteExhaustion) : (s ×ˢ t).FiniteExhaustion

Given K : FiniteExhaustion s and K' : FiniteExhaustion t, FiniteExhaustion.prod K K' is the finite exhaustion on s ×ˢ t given by the pointwise set product of the exhaustions.

Equations

• K.prod K' = { toFun := fun (n : ℕ) => K n ×ˢ K' n, finite' := ⋯, subset_succ' := ⋯, iUnion_eq' := ⋯ }

theorem Set.FiniteExhaustion.prod_apply {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) {β : Type u_2} {t : Set β} (K' : t.FiniteExhaustion) (n : ℕ) : (K.prod K') n = K n ×ˢ K' n