English
If g is an inducing map and f is continuous with g(c•x)=f c • g x, then the action of N on Y is continuous.
Русский
Если g-индуктивно отображает Y в X и существует непрерывная f: N→M с равенством g(c•x)=f c • g x, то действие N на Y непрерывно.
LaTeX
$$IsInducing g → Continuous f → (∀ {c x}, g (c • x) = f c • g x) → ContinuousSMul N Y$$
Lean4
/-- Suppose that `N` acts on `X` and `M` continuously acts on `Y`.
Suppose that `g : Y → X` is an action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c • x) = f c • g x`.
Then the action of `N` on `X` is continuous as well.
In many cases, `f = id` so that `g` is an action homomorphism in the sense of `MulActionHom`.
However, this version also works for semilinear maps and `f = Units.val`. -/
@[to_additive /-- Suppose that `N` additively acts on `X` and `M` continuously additively acts on `Y`.
Suppose that `g : Y → X` is an additive action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c +ᵥ x) = f c +ᵥ g x`.
Then the action of `N` on `X` is continuous as well.
In many cases, `f = id` so that `g` is an action homomorphism in the sense of `AddActionHom`.
However, this version also works for `f = AddUnits.val`. -/
]
theorem continuousSMul {N : Type*} [SMul N Y] [TopologicalSpace N] {f : N → M} (hg : IsInducing g) (hf : Continuous f)
(hsmul : ∀ {c x}, g (c • x) = f c • g x) : ContinuousSMul N Y where
continuous_smul := by
simpa only [hg.continuous_iff, Function.comp_def, hsmul] using
(hf.comp continuous_fst).smul <| hg.continuous.comp continuous_snd
