toNNReal_div — Mathlib

English

For x,y ∈ ℝ with x ≥ 0, Real.toNNReal(x/y) = Real.toNNReal x / Real.toNNReal y.

Русский

Для x ≥ 0, Real.toNNReal(x/y) = Real.toNNReal x / Real.toNNReal y.

LaTeX

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

Lean4

theorem _root_.Real.toNNReal_div {x y : ℝ} (hx : 0 ≤ x) : Real.toNNReal (x / y) = Real.toNNReal x / Real.toNNReal y :=
  by rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]

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