instSecondCountableTopology — Mathlib

English

If G is SecondCountable, then G/N is SecondCountable.

Русский

Если G вторично счётна, то и G/N вторично счётна.

LaTeX

$$[SecondCountableTopology G] ⇒ SecondCountableTopology (HasQuotient.Quotient G N).$$

Lean4

/-- The quotient of a second countable topological group by a subgroup is second countable. -/
@[to_additive /-- The quotient of a second countable additive topological group by a subgroup is second
      countable. -/
    ]
instance instSecondCountableTopology [SecondCountableTopology G] : SecondCountableTopology (G ⧸ N) :=
  ContinuousConstSMul.secondCountableTopology

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