of_coe — Mathlib

English

A Lindelöf set with the discrete topology is countable; more precisely, if s is Lindelöf and carries the discrete topology, then s is countable.

Русский

Если множество с дискретной топологией является Линдельфовым, то оно счетно.

LaTeX

$$$\\text{IsLindelof}(s) \\;\\text{and}\\; \\text{DiscreteTopology}(s)\\;\\Rightarrow\\; s \\text{ is countable}.$$$

Lean4

theorem of_coe [LindelofSpace s] : IsLindelof s :=
  isLindelof_iff_LindelofSpace.mpr ‹_›

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