Documentation

Mathlib.Analysis.Convex.Complex

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}