instSeparableSpaceQuotient — Mathlib

English

If α is a separable space and s a Setoid on α, then the quotient α/ s is separable.

Русский

Если пространства α и множество эквивалентности s сепарабельны, то фактор-пространство α/ s сепарабельно.

LaTeX

$$$[\\text{SeparableSpace } \\alpha] \\Rightarrow \\text{SeparableSpace}(\\operatorname{Quotient} s)$$$

Lean4

instance [SeparableSpace α] {s : Setoid α} : SeparableSpace (Quotient s) :=
  isQuotientMap_quot_mk.separableSpace

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