# 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.

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

A version of `convexHull_prod` for `Set.reProdIm`.

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

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

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

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

source
theorem Complex.starConvex_one_slitPlane :
StarConvex ℝ 1 slitPlane

The slit plane is star-shaped at `1`.

source
theorem convex_halfSpace_re_lt (r : ℝ) :
Convex ℝ {c : ℂ | c.re < r}
source
theorem convex_halfSpace_re_le (r : ℝ) :
Convex ℝ {c : ℂ | c.re ≤ r}
source
theorem convex_halfSpace_re_gt (r : ℝ) :
Convex ℝ {c : ℂ | r < c.re}
source
theorem convex_halfSpace_re_ge (r : ℝ) :
Convex ℝ {c : ℂ | r ≤ c.re}
source
theorem convex_halfSpace_im_lt (r : ℝ) :
Convex ℝ {c : ℂ | c.im < r}
source
theorem convex_halfSpace_im_le (r : ℝ) :
Convex ℝ {c : ℂ | c.im ≤ r}
source
theorem convex_halfSpace_im_gt (r : ℝ) :
Convex ℝ {c : ℂ | r < c.im}
source
theorem convex_halfSpace_im_ge (r : ℝ) :
Convex ℝ {c : ℂ | r ≤ c.im}
source
theorem Complex.isConnected_of_upperHalfPlane {r : ℝ} {s : Set ℂ} (hs₁ : {z : ℂ | r < z.im} ⊆ s) (hs₂ : s ⊆ {z : ℂ | r ≤ z.im}) :
IsConnected s
source
theorem Complex.isConnected_of_lowerHalfPlane {r : ℝ} {s : Set ℂ} (hs₁ : {z : ℂ | z.im < r} ⊆ s) (hs₂ : s ⊆ {z : ℂ | z.im ≤ r}) :
IsConnected s
source
theorem Complex.rectangle_eq_convexHull (z w : ℂ) :
z.Rectangle w = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
source
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.

source
instance Complex.instPathConnectedSpaceUnits :
PathConnectedSpace ℂ ˣ