instContinuousSMulULift — Mathlib

English

If M acts on X with continuous scalar action, then the lifted scalar action on ULift M also acts continuously on X.

Русский

Если у M непрерывно действует на X, то подъём на ULift M сохраняет непрерывность действия на X.

LaTeX

$$$\\text{ContinuousSMul}(\\text{ULift } M)\\, X$$$

Lean4

@[to_additive]
instance : ContinuousSMul (ULift M) X :=
  ⟨(continuous_smul (M := M)).comp₂ (continuous_uliftDown.comp continuous_fst) continuous_snd⟩

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