continuousSMul_compHom — Mathlib

English

If an action is continuous, composing with a continuous monoid homomorphism yields a continuous action.

Русский

Если действие непрерывно, композиция с непрерывным гомоморфизмом моноида даёт непрерывное действие.

LaTeX

$$ContinuousSMul N X$$

Lean4

/-- If an action is continuous, then composing this action with a continuous homomorphism gives
again a continuous action. -/
@[to_additive]
theorem continuousSMul_compHom {N : Type*} [TopologicalSpace N] [Monoid N] {f : N →* M} (hf : Continuous f) :
    letI : MulAction N X := MulAction.compHom _ f
    ContinuousSMul N X :=
  by
  let _ : MulAction N X := MulAction.compHom _ f
  exact ⟨(hf.comp continuous_fst).smul continuous_snd⟩

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