nonpos_iff_exists_ofReal — Mathlib

English

An element z satisfies z ≤ 0 iff there exists a real x ≤ 0 such that z = ofReal(x).

Русский

Элемент z удовлетворяет z ≤ 0 тогда и только тогда, когда существует вещественное число x ≤ 0 такое, что z = ofReal(x).

LaTeX

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

Lean4

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

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