instContinuousMul — Mathlib

English

If a type M is a topological space equipped with a multiplication that is continuous, then the separation quotient of M inherits a multiplication which is continuous, making it a topological semigroup (and related structures) under the induced operation.

Русский

Если M — топологическое пространство с умножением, непрерывным как отображение, то отделение-разделение (SeparationQuotient) M наследует умножение, которое непрерывно, образуя топологическую полугруппу под индукцированной операцией.

LaTeX

$$$\operatorname{ContinuousMul}(\mathrm{SeparationQuotient}(M))$$$

Lean4

@[to_additive]
instance instContinuousMul [Mul M] [ContinuousMul M] : ContinuousMul (SeparationQuotient M) where
  continuous_mul := isQuotientMap_prodMap_mk.continuous_iff.2 <| continuous_mk.comp continuous_mul

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