ofReal_div_of_pos — Mathlib

English

Let x,y ∈ ℝ with y > 0. Then ENNReal.ofReal(x/y) = ENNReal.ofReal x / ENNReal.ofReal y.

Русский

Пусть x,y ∈ ℝ и y > 0. Тогда ENNReal.ofReal(x/y) = ENNReal.ofReal x / ENNReal.ofReal y.

LaTeX

$$$0 < y \Rightarrow ENNReal.ofReal\left(\frac{x}{y}\right) = ENNReal.ofReal(x) / ENNReal.ofReal(y)$$$

Lean4

theorem ofReal_div_of_pos {x y : ℝ} (hy : 0 < y) : ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]

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