isLindelof_sUnion — Mathlib

English

If s is finite and each f_i is Lindelöf, then the union over i∈s of 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_sUnion {S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S) := by
  rw [sUnion_eq_biUnion]; exact hf.isLindelof_biUnion hc

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