Commit 2024-11-10 20:16 984b7316

View on Github →

refactor(Analysis/Complex): merge Complex/Convex and Convex/Complex (#18819) This merges the two files Analysis/Complex/Convex.lean and Analysis/Convex/Complex.lean, putting lemmas about convexity in the complex plane together; and moves a lemma from UpperHalfPlane/Topology.lean to this file, substantially shortening the import path to all the C-star-algebras files.

Estimated changes

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
deleted theorem convex_halfspace_im_ge
deleted theorem convex_halfspace_im_gt
deleted theorem convex_halfspace_im_le
deleted theorem convex_halfspace_im_lt
deleted theorem convex_halfspace_re_ge
deleted theorem convex_halfspace_re_gt
deleted theorem convex_halfspace_re_le
deleted theorem convex_halfspace_re_lt