instContinuousMul — Mathlib

English

If SMulCommClass holds for M,N on X with uniform continuous smuls, then it holds on Completion X.

Русский

Если SMulCommClass выполняется на X для M и N с равномерно непрерывными умножениями, то оно выполняется и на Completion X.

LaTeX

$$$\\text{SMulCommClass } M N (\\mathrm{Completion}(X))$$$

Lean4

instance : ContinuousMul (Completion α) where
  continuous_mul := by
    let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
    have : Continuous fun p : α × α => m p.1 p.2 := (continuous_coe α).comp continuous_mul
    have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
    exact (di.extend_Z_bilin di this :)

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