English
If f is a map between spaces with a compatible topological structure, then the induced action on the domain yields a continuous scalar action.
Русский
Если имеет место отображение между пространствами с совместной топологией, индуцированное действие скаляра на область является непрерывным.
LaTeX
$$$\\text{ContinuousSMul}(R,\\alpha)$, индукция топологий через f$$
Lean4
theorem induced {R : Type*} {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Semiring R] [AddCommMonoid α]
[AddCommMonoid β] [Module R α] [Module R β] [TopologicalSpace R] [LinearMapClass F R α β] [tβ : TopologicalSpace β]
[ContinuousSMul R β] (f : F) : @ContinuousSMul R α _ _ (tβ.induced f) :=
by
let tα := tβ.induced f
refine ⟨continuous_induced_rng.2 ?_⟩
simp only [Function.comp_def, map_smul]
fun_prop
