feat(Data/Complex/Order, Analysis/Complex/Basic): add OrderClosedTopo…

…logy instance, monotonicity of ofReal (#10112)

This adds an `OrderClosedTopology` instance (scoped to `ComplexOrder`) for the complex numbers (to make things like `tsum_le_tsum` work with the partial order on the complex numbers) and the fact that `Complex.ofReal'` is monotone with respect to this order.



Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Mathlib/Analysis/Complex/Basic.lean

@@ -491,6 +491,15 @@ theorem eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) : z = ↑‖z‖ := by
   rw [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg (id hz.1 : 0 ≤ z)]
 #align complex.eq_coe_norm_of_nonneg Complex.eq_coe_norm_of_nonneg
 
+/-- We show that the partial order and the topology on `ℂ` are compatible.
+We turn this into an instance scoped to `ComplexOrder`. -/
+lemma orderClosedTopology : OrderClosedTopology ℂ where
+  isClosed_le' := by
+    simp_rw [le_def, Set.setOf_and]
+    refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> continuity
+
+scoped[ComplexOrder] attribute [instance] Complex.orderClosedTopology
+
 end ComplexOrder
 
 end Complex

Mathlib/Data/Complex/Order.lean

@@ -115,4 +115,8 @@ lemma neg_re_eq_abs {z : ℂ} : -z.re = abs z ↔ z ≤ 0 := by
 @[simp]
 lemma re_eq_neg_abs {z : ℂ} : z.re = -abs z ↔ z ≤ 0 := by rw [← neg_eq_iff_eq_neg, neg_re_eq_abs]
 
+lemma monotone_ofReal : Monotone ofReal' := by
+  intro x y hxy
+  simp only [ofReal_eq_coe, real_le_real, hxy]
+
 end Complex