Complex.le_def

theorem Complex.le_def : ∀ {z w : ℂ}, z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im

This theorem states that for any two complex numbers `z` and `w`, `z` is less than or equal to `w` if and only if the real part of `z` is less than or equal to the real part of `w` and the imaginary part of `z` is equal to the imaginary part of `w`. In other words, in the context of complex numbers, the inequality `z ≤ w` is defined by comparing their real parts and checking for equality of their imaginary parts.

More concisely: For complex numbers z and w, z <= w if and only if Re(z) <= Re(w) and Im(z) = Im(w).