pos_iff_exists_ofReal — Mathlib

English

An element z is positive if and only if there exists a real x > 0 such that z equals the image of x under the real embedding.

Русский

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

LaTeX

$$$ 0 < z \iff \exists x > 0, z = \operatorname{ofReal}(x) $$$

Lean4

theorem pos_iff_exists_ofReal : 0 < z ↔ ∃ x > (0 : ℝ), x = z := by simp_rw [pos_iff (K := K), ext_iff (K := K)]; aesop

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