nonneg_iff_exists_ofReal — Mathlib

English

An element z is nonnegative if and only if there exists a real x ≥ 0 such that z is the image of x under the real-embedding map.

Русский

Элемент z неотрицателен тогда и только тогда, существует вещественное число x ≥ 0 такое, что z является образием x под отображением вещественного включения.

LaTeX

$$$ 0 \le z \iff \exists x \ge 0, z = \operatorname{ofReal}(x) $$$

Lean4

theorem nonneg_iff_exists_ofReal : 0 ≤ z ↔ ∃ x ≥ (0 : ℝ), x = z := by simp_rw [nonneg_iff (K := K), ext_iff (K := K)];
  aesop

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