English
Let z and w be elements of a complex-like ordered system. Then z is less than w precisely when their real parts satisfy Re(z) < Re(w) and their imaginary parts are equal.
Русский
Пусть z и w принадлежат комплексоподобной упорядоченной системе. Тогда z < w тогда и только тогда, когда Re(z) < Re(w) и Im(z) = Im(w).
LaTeX
$$$ z < w \iff \operatorname{re}(z) < \operatorname{re}(w) \land \operatorname{im}(z) = \operatorname{im}(w) $$$
Lean4
theorem lt_iff_re_im : z < w ↔ re z < re w ∧ im z = im w :=
by
simp_rw [lt_iff_le_and_ne, @RCLike.le_iff_re_im K]
constructor
· rintro ⟨⟨hr, hi⟩, heq⟩
exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩
· rintro ⟨⟨hr, hrn⟩, hi⟩
exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩
