Theorems about convexity on the complex plane

We show that the open and closed half-spaces in ℂ given by an inequality on either the real or imaginary part are all convex over ℝ. We also prove some results on star-convexity for the slit plane.

theorem Complex.convexHull_reProdIm (s t : Set ℝ) : (convexHull ℝ) (s ×ℂ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t

A version of convexHull_prod for Set.reProdIm.

theorem Complex.starConvex_slitPlane {z : ℂ} (hz : 0 < z) : StarConvex ℝ z slitPlane

The slit plane is star-convex at a positive number.

theorem Complex.starConvex_ofReal_slitPlane {x : ℝ} (hx : 0 < x) : StarConvex ℝ (↑x) slitPlane

The slit plane is star-shaped at a positive real number.

theorem Complex.starConvex_one_slitPlane : StarConvex ℝ 1 slitPlane

The slit plane is star-shaped at 1.

theorem convex_halfSpace_re_lt (r : ℝ) : Convex ℝ {c : ℂ | c.re < r}

theorem convex_halfSpace_re_le (r : ℝ) : Convex ℝ {c : ℂ | c.re ≤ r}

theorem convex_halfSpace_re_gt (r : ℝ) : Convex ℝ {c : ℂ | r < c.re}

theorem convex_halfSpace_re_ge (r : ℝ) : Convex ℝ {c : ℂ | r ≤ c.re}

theorem convex_halfSpace_im_lt (r : ℝ) : Convex ℝ {c : ℂ | c.im < r}

theorem convex_halfSpace_im_le (r : ℝ) : Convex ℝ {c : ℂ | c.im ≤ r}

theorem convex_halfSpace_im_gt (r : ℝ) : Convex ℝ {c : ℂ | r < c.im}

theorem convex_halfSpace_im_ge (r : ℝ) : Convex ℝ {c : ℂ | r ≤ c.im}

theorem Complex.isConnected_of_upperHalfPlane {r : ℝ} {s : Set ℂ} (hs₁ : {z : ℂ | r < z.im} ⊆ s) (hs₂ : s ⊆ {z : ℂ | r ≤ z.im}) : IsConnected s

theorem Complex.isConnected_of_lowerHalfPlane {r : ℝ} {s : Set ℂ} (hs₁ : {z : ℂ | z.im < r} ⊆ s) (hs₂ : s ⊆ {z : ℂ | z.im ≤ r}) : IsConnected s

theorem Complex.rectangle_eq_convexHull (z w : ℂ) : z.Rectangle w = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}

theorem Complex.Convex.rectangle_subset {U : Set ℂ} (U_convex : Convex ℝ U) {z w : ℂ} (hz : z ∈ U) (hw : w ∈ U) (hzw : ↑z.re + ↑w.im * I ∈ U) (hwz : ↑w.re + ↑z.im * I ∈ U) : z.Rectangle w ⊆ U

If opposite corners of a rectangle are contained in a convex set, the whole rectangle is.

instance Complex.instPathConnectedSpaceUnits : PathConnectedSpace ℂˣ