secondCountableTopology — Mathlib

English

The quotient by a group action of a second-countable space is itself second-countable.

Русский

Квотиент группы пространства с счетной базой сохраняет счетность.

LaTeX

$$$SecondCountableTopology (Quotient (MulAction.orbitRel \Gamma T))$$$

Lean4

/-- The quotient of a second countable space by a group action is second countable. -/
@[to_additive /-- The quotient of a second countable space by an additive group action is second
    countable. -/
    ]
theorem secondCountableTopology [SecondCountableTopology T] [ContinuousConstSMul Γ T] :
    SecondCountableTopology (Quotient (MulAction.orbitRel Γ T)) :=
  TopologicalSpace.Quotient.secondCountableTopology isOpenMap_quotient_mk'_mul

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