ofReal_nsmul — Mathlib

English

For any x ∈ ℝ and n ∈ ℕ, ENNReal.ofReal(n • x) = n • ENNReal.ofReal(x).

Русский

Для любых x ∈ ℝ и n ∈ ℕ: ENNReal.ofReal(n • x) = n • ENNReal.ofReal(x).

LaTeX

$${x : ℝ} {n : ℕ} ⇒ \operatorname{ofReal}(n \cdot x) = n \cdot \operatorname{ofReal}(x)$$

Lean4

theorem ofReal_nsmul {x : ℝ} {n : ℕ} : ENNReal.ofReal (n • x) = n • ENNReal.ofReal x := by
  simp only [nsmul_eq_mul, ← ofReal_natCast n, ← ofReal_mul n.cast_nonneg]

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