continuousMul_induced — Mathlib

English

For any f, the induced topology on M yields a continuous multiplication provided the target supports a continuous multiplication and f is appropriate.

Русский

Для любого f индуцированная топология на M обеспечивает непрерывное умножение, если цель поддерживает непрерывное умножение и f удовлетворяет условиям.

LaTeX

$$continuousMul_induced {M N F} … : @ContinuousMul M (induced f ‹_›) _$$

Lean4

@[to_additive]
theorem continuousMul_induced {M N F : Type*} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace N]
    [ContinuousMul N] (f : F) : @ContinuousMul M (induced f ‹_›) _ :=
  letI := induced f ‹_›
  IsInducing.continuousMul f ⟨rfl⟩

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