isLindelof_iff_countable — Mathlib

English

In a discrete space, a subset is Lindelöf if and only if it is countable.

Русский

В дискретном пространстве подмножество Линдельоф тогда и только тогда, когда оно счётно.

LaTeX

$$$[DiscreteTopology X] \ IsLindelof\,s \iff s.Countable$$$

Lean4

theorem isLindelof_iff_countable [DiscreteTopology X] : IsLindelof s ↔ s.Countable :=
  ⟨fun h => h.countable_of_discrete, fun h => h.isLindelof⟩

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