separableSpace_iff_countable — Mathlib

English

Let α be a type endowed with the discrete topology. Then α is separable if and only if α is countable.

Русский

Пусть α — множество с дискретной топологией. Тогда α сепарабельно тогда и только тогда, когда α счётно.

LaTeX

$$$SeparableSpace\ α \iff Countable\ α$$$

Lean4

/-- A topological space with discrete topology is separable iff it is countable. -/
theorem separableSpace_iff_countable [DiscreteTopology α] : SeparableSpace α ↔ Countable α := by
  simp [separableSpace_iff, countable_univ_iff]

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