mk_of_countable_eventually_mem — Mathlib

English

If a space is covered by countably many sets each of cardinality a, then the space has cardinality exactly a.

Русский

Если пространство покрыто счётным семейством множеств, каждое кардинальности a, то кардинальность пространства равна a.

LaTeX

$$$\#\alpha = a$$$

Lean4

/-- If a space is eventually covered by a countable family of sets, all with cardinality `a`,
then the cardinality of the space is also `a`. -/
theorem mk_of_countable_eventually_mem {α : Type u} {ι : Type v} {a : Cardinal} [Countable ι] {f : ι → Set α}
    {l : Filter ι} [NeBot l] (ht : ∀ x, ∀ᶠ i in l, x ∈ f i) (h'f : ∀ i, #(f i) = a) : #α = a :=
  by
  apply le_antisymm
  · apply mk_le_of_countable_eventually_mem ht (fun i ↦ (h'f i).le)
  · obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l
    rw [← (h'f i)]
    exact mk_set_le (f i)

Похожие утверждения