Convexity of half spaces in ℂ

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 : ℝ) : Convex ℝ {c : ℂ | c.re ≤ r}

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

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

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

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

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

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