separableSpace — Mathlib

English

If the domain α is separable, then β is separable as soon as e is a dense embedding.

Русский

Если домен α сепарабельное пространство и e — плотное вложение, то β сепарабельное.

LaTeX

$$$SeparableSpace α \\Rightarrow IsDenseEmbedding e \\Rightarrow SeparableSpace β$$$

Lean4

/-- If the domain of a `IsDenseEmbedding` is a separable space, then so is its codomain. -/
protected theorem separableSpace [SeparableSpace α] (de : IsDenseEmbedding e) : SeparableSpace β :=
  de.isDenseInducing.separableSpace

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