instDiscreteTopologyQuotientOfContinuousMul

English

Under a continuous multiplication on G, the quotient by an openSubgroup U has discrete topology.

Русский

При непрерывном умножении на группе G, фактор-группа по открытой подгруппе U имеет дискретную топологию.

LaTeX

$$$$ \\text{DiscreteTopology}(G/U) \\text{ for open } U. $$$$

Lean4

@[to_additive]
instance [ContinuousMul G] (U : OpenSubgroup G) : DiscreteTopology (G ⧸ U.toSubgroup) :=
  discreteTopology U.toSubgroup U.isOpen

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