not_lt_iff — Mathlib

English

Let z, w be complex numbers. The negation of z < w is equivalent to either w.re ≤ z.re or z.im ≠ w.im.

Русский

Пусть z, w — комплексные числа. Отрицание неравенства z < w эквивалентно тому, что либо w.re ≤ z.re, либо z.im ≠ w.im.

LaTeX

$$$\neg z < w \iff w.re \le z.re \lor z.im \neq w.im$$$

Lean4

theorem not_lt_iff {z w : ℂ} : ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im := by rw [lt_def, not_and_or, not_lt]

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