coe_ennreal_nsmul — Mathlib

English

The embedding commutes with natural-number scalar multiplication: (n • x) in ENNReal maps to n • (x:EReal).

Русский

Вложение коммутирует умножение на натуральное число: n • x в ENNReal сопоставляется n • (x:EReal).

LaTeX

$$$$ (n \cdot x)^{EReal} = n \cdot (x^{EReal}), \; n \in \mathbb{N}, \; x \in ENNReal. $$$$

Lean4

@[norm_cast]
theorem coe_ennreal_nsmul (n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : EReal) = n • (x : EReal) :=
  map_nsmul (⟨⟨(↑), coe_ennreal_zero⟩, coe_ennreal_add⟩ : ℝ≥0∞ →+ EReal) _ _

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