mk_le_of_countable_eventually_mem

English

If a space is eventually covered by a countable family of sets, each of cardinality at most a, then the cardinality of the space is at most a.

Русский

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

LaTeX

$$$\#\alpha \le a$$$

Lean4

/-- If a space is eventually covered by a countable family of sets, all with cardinality at
most `a`, then the cardinality of the space is also bounded by `a`. -/
theorem mk_le_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
  rw [← mk_univ]
  exact mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f

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