instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd

English

Under suitable topological algebraic hypotheses (R a topological semiring and M a topological R-bimodule with continuous actions), the multiplication on tsze R M is continuous.

Русский

При подходящих условия топологической алгебры (R — топологический полукольцо, M — топологический R-би-модуль с непрерывными действиями), умножение на tsze R M непрерывно.

LaTeX

$$$\\operatorname{ContinuousMul}(\\mathrm{tsze}(R,M))$$$

Lean4

instance [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] [ContinuousMul R] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M]
    [ContinuousAdd M] : ContinuousMul (tsze R M) :=
  ⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prodMk <|
      ((continuous_fst.comp continuous_fst).smul (continuous_snd.comp continuous_snd)).add
        ((MulOpposite.continuous_op.comp <| continuous_fst.comp <| continuous_snd).smul
          (continuous_snd.comp continuous_fst))⟩

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