English
If β is a topological space with continuous multiplication and α is equipped with the induced topology via f: α → β, then α carries a continuous multiplication making it a topological monoid.
Русский
Если β — топологическое пространство с непрерывным умножением и α обладает индуцированной топологией через f: α→β, то α наследует непрерывное умножение и образует топологическую моноиду.
LaTeX
$$$\text{ContinuousMul}$ (induced $\alpha$ via $f$) $\Rightarrow$ $\text{ContinuousMul}(\alpha)$$$
Lean4
@[to_additive]
theorem induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Mul α] [Mul β] [MulHomClass F α β]
[tβ : TopologicalSpace β] [ContinuousMul β] (f : F) : @ContinuousMul α (tβ.induced f) _ :=
by
let tα := tβ.induced f
refine ⟨continuous_induced_rng.2 ?_⟩
simp only [Function.comp_def, map_mul]
fun_prop
