English
If g : β → α is an inducing map and there is a family of maps f : N → M such that g(c • x) = f(c) • g(x) for all c and x, then there is a continuous constant smul on β.
Русский
Если g : β → α индукционирует (индуцирует) отображение и существует семейство отображений f : N → M такое, что g(c • x) = f(c) • g(x) для всех c и x, тогда на β существует непрерывное константное умножение.
LaTeX
$$$ \\mathrm{IsInducing}(g) \\Rightarrow \\forall f:\\, N \\to M, \\ \\forall c, x,\\ g(c \\cdot x) = f(c) \\cdot g(x) \\Rightarrow \\mathrm{ContinuousConstSMul}(N, \\beta) $$$
Lean4
@[to_additive]
theorem continuousConstSMul {N β : Type*} [SMul N β] [TopologicalSpace β] {g : β → α} (hg : IsInducing g) (f : N → M)
(hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x) : ContinuousConstSMul N β where
continuous_const_smul
c := by simpa only [Function.comp_def, hf, hg.continuous_iff] using hg.continuous.const_smul (f c)
