English
The order relation on ℂ is given by z ≤ w iff and only if z.re ≤ w.re and z.im = w.im.
Русский
Порядок на ℂ задаётся так: z ≤ w тогда и только тогда, когда z.re ≤ w.re и z.im = w.im.
LaTeX
$$$z \\le w \\iff z_{\\mathrm{re}} \\le w_{\\mathrm{re}} \\wedge z_{\\mathrm{im}} = w_{\\mathrm{im}}$$$
Lean4
/-- We put a partial order on ℂ so that `z ≤ w` exactly if `w - z` is real and nonnegative.
Complex numbers with different imaginary parts are incomparable.
-/
protected def partialOrder : PartialOrder ℂ
where
le z w := z.re ≤ w.re ∧ z.im = w.im
lt z w := z.re < w.re ∧ z.im = w.im
lt_iff_le_not_ge z
w := by
rw [lt_iff_le_not_ge]
tauto
le_refl _ := ⟨le_rfl, rfl⟩
le_trans _ _ _ h₁ h₂ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩
le_antisymm _ _ h₁ h₂ := ext (h₁.1.antisymm h₂.1) h₁.2
