Theorems about convexity on the complex plane

theorem Complex.convexHull_reProdIm (s : Set ℝ) (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 Complex.slitPlane

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

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

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

theorem Complex.starConvex_one_slitPlane : StarConvex ℝ 1 Complex.slitPlane

The slit plane is star-shaped at 1.