instMulActionNNReal — Mathlib

English

A scalar action of ENNReal on a space M restricts to a scalar action of NNReal on M.

Русский

Действие скаляра ENNReal на пространство M ограничивает действие NNReal на M.

LaTeX

$$$\\text{ENNReal.instMulActionNNReal}\\ :\\ \\mathrm{MulAction} \\ NNReal\\ M$$$

Lean4

/-- A `MulAction` over `ℝ≥0∞` restricts to a `MulAction` over `ℝ≥0`. -/
noncomputable instance {M : Type*} [MulAction ℝ≥0∞ M] : MulAction ℝ≥0 M :=
  MulAction.compHom M ofNNRealHom.toMonoidHom

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