toNNReal_div' — Mathlib

English

If y ≥ 0, Real.toNNReal(x/y) = Real.toNNReal x / Real.toNNReal y.

Русский

Если y ≥ 0, Real.toNNReal(x/y) = Real.toNNReal x / Real.toNNReal y.

LaTeX

$$$\forall x,y \in \mathbb{R},\ y \ge 0\Rightarrow Real.toNNReal(x/y) = Real.toNNReal x / Real.toNNReal y$$$

Lean4

theorem _root_.Real.toNNReal_div' {x y : ℝ} (hy : 0 ≤ y) : Real.toNNReal (x / y) = Real.toNNReal x / Real.toNNReal y :=
  by rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]

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