English
Let M be an AddMonoid equipped with a distributive action of ENNReal. Then M carries a natural action of NNReal obtained by restricting ENNReal's action along the inclusion NNReal → ENNReal.
Русский
Пусть M параз AddMonoid с распределенным действием ℝ≥0∞ на M. Тогда на M естественно определяется действие NNReal, полученное ограничением действия ℝ≥0∞ по включению NNReal ↪ ℝ≥0∞.
LaTeX
$$$\text{Restrict}_{\mathbb{R}_{\ge 0}}^{\mathbb{R}_{\ge 0^\infty}}(M)\text{ with } r \cdot m := (\operatorname{ofNNReal} r) \cdot m.$$$
Lean4
/-- A `DistribMulAction` over `ℝ≥0∞` restricts to a `DistribMulAction` over `ℝ≥0`. -/
noncomputable instance {M : Type*} [AddMonoid M] [DistribMulAction ℝ≥0∞ M] : DistribMulAction ℝ≥0 M :=
DistribMulAction.compHom M ofNNRealHom.toMonoidHom
