isLindelof_iUnion — Mathlib

English

Let X be a topological space and ι a countable index set. If each f(i) is a Lindelöf subset of X, then the union ⋃ i f(i) is Lindelöf.

Русский

Пусть X — топологическое пространство, ι — счётный индексный набор. Пусть каждый f(i) является множеством Линдельоф в X, тогда объединение ⋃_{i} f(i) также Линдельоф.

LaTeX

$$$\Bigl( \iota \text{ is countable} \;\wedge\; \forall i, \ IsLindelof(f(i)) \Bigr) \Rightarrow IsLindelof\left(\bigcup_i f(i)\right)$$$

Lean4

theorem isLindelof_iUnion {ι : Sort*} {f : ι → Set X} [Countable ι] (h : ∀ i, IsLindelof (f i)) :
    IsLindelof (⋃ i, f i) :=
  (countable_range f).isLindelof_sUnion <| forall_mem_range.2 h

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