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}

@[deprecated convex_halfSpace_re_lt (since := "2024-11-12")]

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

Alias of convex_halfSpace_re_lt.

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

@[deprecated convex_halfSpace_re_le (since := "2024-11-12")]

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

Alias of convex_halfSpace_re_le.

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

@[deprecated convex_halfSpace_re_gt (since := "2024-11-12")]

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

Alias of convex_halfSpace_re_gt.

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

@[deprecated convex_halfSpace_re_ge (since := "2024-11-12")]

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

Alias of convex_halfSpace_re_ge.

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

@[deprecated convex_halfSpace_im_lt (since := "2024-11-12")]

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

Alias of convex_halfSpace_im_lt.

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

@[deprecated convex_halfSpace_im_le (since := "2024-11-12")]

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

Alias of convex_halfSpace_im_le.

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

@[deprecated convex_halfSpace_im_gt (since := "2024-11-12")]

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

Alias of convex_halfSpace_im_gt.

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

@[deprecated convex_halfSpace_im_ge (since := "2024-11-12")]

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

Alias of convex_halfSpace_im_ge.

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