mathlib3 documentation

analysis.convex.complex

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 : ) :
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}