instContinuousConstSMul — Mathlib

English

If M acts on X with continuous constant smul, then the induced ContinuousConstSMul on SeparationQuotient X is continuous.

Русский

Если M действует на X непрерывно константно, то на SeparationQuotient X индуцированное непрерывное константное умножение непрерывно.

LaTeX

$$ContinuousConstSMul M (SeparationQuotient X)$$

Lean4

@[to_additive]
instance instContinuousConstSMul : ContinuousConstSMul M (SeparationQuotient X) where
  continuous_const_smul c := isQuotientMap_mk.continuous_iff.2 <| continuous_mk.comp <| continuous_const_smul c

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