ofReal_lt_zero — Mathlib

English

For any real x, its image under the canonical embedding into a real-closed-like structure K preserves order with respect to 'less than zero': x < 0 iff the embedded element is < 0.

Русский

Для любого действительного числа x его образ в структуры K сохраняет порядок: x < 0 тогда и только тогда, когда образ в K тоже меньше нуля.

LaTeX

$$$\\forall x\\in\\mathbb{R},\\; (x)_{K} < 0 \\iff x < 0$$$

Lean4

@[simp, norm_cast]
theorem ofReal_lt_zero {x : ℝ} : (x : K) < 0 ↔ x < 0 := by rw [← ofReal_zero, ofReal_lt_ofReal]

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