toNNReal_le_toNNReal_iff' — Mathlib

English

For all r, p ∈ ℝ, we have r.toNNReal ≤ p.toNNReal iff (r ≤ p) or (r ≤ 0).

Русский

Для всех r, p ∈ ℝ выполняется r.toNNReal ≤ p.toNNReal эквивалентно (r ≤ p) или (r ≤ 0).

LaTeX

$$$$ \operatorname{toNNReal}(r) \le \operatorname{toNNReal}(p) \iff r \le p \lor r \le 0. $$$$

Lean4

theorem toNNReal_le_toNNReal_iff' {r p : ℝ} : r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0 := by
  simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]

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