Commit 2023-05-03 01:24 650121b5

View on Github →

feat: port Analysis.Convex.Complex (#3763)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Complex.lean

added theorem convex_halfspace_im_ge

added theorem convex_halfspace_im_gt

added theorem convex_halfspace_im_le

added theorem convex_halfspace_im_lt

added theorem convex_halfspace_re_ge

added theorem convex_halfspace_re_gt

added theorem convex_halfspace_re_le

added theorem convex_halfspace_re_lt