isLindelof_iff_LindelofSpace — Mathlib

English

For any subset s ⊆ X, IsLindelof s is equivalent to IsLindelof(s.Elem) where s.Elem denotes the subtype representation; i.e., s is Lindelöf iff the subspace s is Lindelöf.

Русский

Для подмножества s ⊆ X эквивалентно IsLindelof s и IsLindelof(subspace s); то есть s Линдельфово тогда и только тогда, когда подпространство s Линдельфово.

LaTeX

$$$\\operatorname{IsLindelof}(s) \\iff \\operatorname{LindelofSpace}(s.Elem).$$$

Lean4

theorem isLindelof_iff_LindelofSpace : IsLindelof s ↔ LindelofSpace s :=
  isLindelof_iff_isLindelof_univ.trans isLindelof_univ_iff

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