ofReal_nonneg — Mathlib

English

Nonnegativity of embedded reals is preserved: 0 ≤ (x : K) iff 0 ≤ x for real x.

Русский

Неотрицательность встроенного вещественного числа сохраняется: 0 ≤ (x : K) тогда и только тогда, когда 0 ≤ x для вещественного x.

LaTeX

$$$ 0 \le (x : K) \iff 0 \le x $$$

Lean4

@[simp, norm_cast]
theorem ofReal_nonneg {x : ℝ} : 0 ≤ (x : K) ↔ 0 ≤ x := by rw [← ofReal_zero, ofReal_le_ofReal]

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