instSeparableSpace — Mathlib

English

If M is a separable topological space, then the DomMulAct space Mᵈᵐᵃ is separable.

Русский

Пусть M — сепарабельное топологическое пространство. Тогда пространство DomMulAct M сепарабельное.

LaTeX

$$$$ \operatorname{SeparableSpace}(M) \Rightarrow \operatorname{SeparableSpace}(\mathrm{DomMulAct}(M)) $$$$

Lean4

@[to_additive]
instance instSeparableSpace [SeparableSpace M] : SeparableSpace Mᵈᵐᵃ :=
  isQuotientMap_mk.separableSpace

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