isSeparable_iff — Mathlib

English

If s is dense, then IsSeparable s is equivalent to SeparableSpace α.

Русский

Если s плотна в пространстве, то IsSeparable s эквивалентно SeparableSpace α.

LaTeX

$$$Dense\ s \Rightarrow (IsSeparable\ s \iff SeparableSpace\ α)$$$

Lean4

theorem _root_.Dense.isSeparable_iff (hs : Dense s) : IsSeparable s ↔ SeparableSpace α := by
  simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff, ← hs.closure_eq,
    isClosed_closure.closure_subset_iff]

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