isLindelof_biUnion — Mathlib

English

For a finite set s of indices, the union over i∈s of f_i is Lindelöf if each 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 : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsLindelof (f i)) :
    IsLindelof (⋃ i ∈ s, f i) :=
  s.finite_toSet.isLindelof_biUnion hf

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