continuousMul — Mathlib

English

If f induces a topology on M from another type and that other type has a continuous multiplication, then M with the induced topology also has a continuous multiplication.

Русский

Если гомоморфизм f порождает топологию на M из другой области, и эта область имеет непрерывное умножение, то и M с индуцированной топологией имеет непрерывное умножение.

LaTeX

$$$\\text{continuousMul}\\ M$ for the induced topology by f when IsInducing f$$

Lean4

@[to_additive]
theorem continuousMul {M N F : Type*} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace M]
    [TopologicalSpace N] [ContinuousMul N] (f : F) (hf : IsInducing f) : ContinuousMul M :=
  ⟨(hf.continuousSMul hf.continuous (map_mul f _ _)).1⟩

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