Documentation

Mathlib.Analysis.Complex.Convex

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.

A version of convexHull_prod for Set.reProdIm.

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

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

The slit plane is star-shaped at 1.

theorem Complex.isConnected_of_upperHalfPlane {r : } {s : Set } (hs₁ : {z : | r < z.im} s) (hs₂ : s {z : | r z.im}) :
theorem Complex.isConnected_of_lowerHalfPlane {r : } {s : Set } (hs₁ : {z : | z.im < r} s) (hs₂ : s {z : | z.im r}) :