The partial order on the complex numbers

This order is defined by z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im.

This is a natural order on ℂ because, as is well-known, there does not exist an order on ℂ making it into a LinearOrderedField. However, the order described above is the canonical order stemming from the structure of ℂ as a ⋆-ring (i.e., it becomes a StarOrderedRing). Moreover, with this order ℂ is a StrictOrderedCommRing and the coercion (↑) : ℝ → ℂ is an order embedding.

This file only provides Complex.partialOrder and lemmas about it. Further structural classes are provided by Mathlib/Data/IsROrC/Basic.lean as

• IsROrC.toStrictOrderedCommRing
• IsROrC.toStarOrderedRing
• IsROrC.toOrderedSMul

These are all only available with open scoped ComplexOrder.

def Complex.partialOrder : PartialOrder ℂ

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.

Equations

• Complex.partialOrder = PartialOrder.mk Complex.partialOrder.proof_4

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

theorem Complex.lt_def {z : ℂ} {w : ℂ} : z < w ↔ z.re < w.re ∧ z.im = w.im

@[simp]

theorem Complex.real_le_real {x : ℝ} {y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Complex.real_lt_real {x : ℝ} {y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem Complex.zero_le_real {x : ℝ} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Complex.zero_lt_real {x : ℝ} : 0 < ↑x ↔ 0 < x

theorem Complex.not_le_iff {z : ℂ} {w : ℂ} : ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

theorem Complex.not_lt_iff {z : ℂ} {w : ℂ} : ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

theorem Complex.not_le_zero_iff {z : ℂ} : ¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0

theorem Complex.not_lt_zero_iff {z : ℂ} : ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0

theorem Complex.eq_re_ofReal_le {r : ℝ} {z : ℂ} (hz : ↑r ≤ z) : z = ↑z.re