separableSpace_univ — Mathlib

English

If α is a separable space, then the universal subset univ ⊆ α, viewed as a subspace, is also separable.

Русский

Если пространство α сепарабельно, то его единичное подмножество univ, рассматриваемое как подпространство, также сепарабельно.

LaTeX

$$$\mathrm{SeparableSpace}(\mathrm{univ} : \mathrm{Set}\,\alpha)$$$

Lean4

instance separableSpace_univ {α : Type*} [TopologicalSpace α] [SeparableSpace α] : SeparableSpace (univ : Set α) :=
  (Equiv.Set.univ α).symm.surjective.denseRange.separableSpace (continuous_id.subtype_mk _)

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