isLindelof_sUnion — Mathlib

English

A set s is Lindelöf if for every family of closed sets t_i, if s ∩ ⋂ t_i = ∅ then there exists a countable subfamily with empty intersection.

Русский

Множество s Линдельёфово, если для любой семьи замкнутых множеств t_i выполняется, что s ∩ ⋂ t_i = ∅ тогда существует счётное подподмножество с пустым пересечением.

LaTeX

$$$IsLindelof(s) \iff \\ ∀ t_i \ (IsClosed(t_i)) \to (s \cap \bigcap_i t_i = \emptyset) \to ∃ u \subseteq I, u.Countable ∧ (s \cap \bigcap_{i∈u} t_i) = \emptyset.$$$

Lean4

theorem isLindelof_sUnion {S : Set (Set X)} (hf : S.Countable) (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S) := by
  rw [sUnion_eq_biUnion]; exact hf.isLindelof_biUnion hc

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