Convexity of half spaces in ℂ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The open and closed half-spaces in ℂ given by an inequality on either the real or imaginary part are all convex over ℝ.

theorem convex_halfspace_re_lt (r : ℝ) :

convex ℝ {c : ℂ | c.re < r}

theorem convex_halfspace_re_le (r : ℝ) :

theorem convex_halfspace_re_gt (r : ℝ) :

convex ℝ {c : ℂ | r < c.re}

theorem convex_halfspace_re_ge (r : ℝ) :

theorem convex_halfspace_im_lt (r : ℝ) :

convex ℝ {c : ℂ | c.im < r}

theorem convex_halfspace_im_le (r : ℝ) :

theorem convex_halfspace_im_gt (r : ℝ) :

convex ℝ {c : ℂ | r < c.im}

theorem convex_halfspace_im_ge (r : ℝ) :