isLindelof_biUnion — Mathlib

English

If s is finite and each f_i is Lindelöf, then the union ⋃_{i∈s} f_i is Lindelöf.

Русский

Если s конечно и каждый f_i Линдельёфово, то объединение ⋃_{i∈s} f_i Линдельёфово.

LaTeX

$$$s\text{ finite} \to (\forall i\in s, IsLindelof(f_i)) \to IsLindelof(\bigcup_{i\in s} f_i).$$$

Lean4

theorem isLindelof_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Finite) (hf : ∀ i ∈ s, IsLindelof (f i)) :
    IsLindelof (⋃ i ∈ s, f i) :=
  Set.Countable.isLindelof_biUnion (countable hs) hf

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