Commit 2024-11-13 06:19 9be022ad

View on Github →

chore: rename halfspace to halfSpace (#18935) Rename halfspace to halfSpace, treating half and space as two words. This conforms to the existing pattern in

  • EuclideanHalfSpace
  • UpperHalfPlane
  • HalfPlane.lean

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
added theorem convex_halfSpace_ge
added theorem convex_halfSpace_gt
added theorem convex_halfSpace_le
added theorem convex_halfSpace_lt
deleted theorem convex_halfspace_ge
deleted theorem convex_halfspace_gt
deleted theorem convex_halfspace_le
deleted theorem convex_halfspace_lt
added theorem iInter_halfSpaces_eq
deleted theorem iInter_halfspaces_eq
added theorem closure_halfSpace
deleted theorem closure_halfspace
added theorem closure_open_halfSpace
deleted theorem closure_open_halfspace
added theorem frontier_halfSpace
deleted theorem frontier_halfspace
added theorem interior_halfSpace
deleted theorem interior_halfspace