instContinuousSMul — Mathlib

English

The quotient space G/N carries a continuous action of G: for every fixed g ∈ G, the map x̄ ↦ g x̄ on G/N is continuous.

Русский

Фактор-пространство G/N наследует непрерывное действие от G: для каждого фиксированного элемента g ∈ G отображение x̄ ↦ g x̄ на G/N непрерывно.

LaTeX

$$$\forall g \in G,\; (\overline{x} \mapsto g \cdot \overline{x}) \text{ is continuous on } G/N.$$$

Lean4

@[to_additive]
instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
  continuous_smul := by
    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul

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