Commit 2026-10-19 03:53 92909395

View on Github →

chore(Geometry/Manifold): missing lemmas about quadrants (#44352) Adds a few lemmas that exist for the half-space, but not quadrants and cleans up the naming.

Estimated changes

Modified Mathlib/Geometry/Manifold/Instances/Real.lean

added theorem closure_quadrant

added theorem frontier_quadrant

added theorem frontier_range_modelWithCornersEuclideanQuadrant

deleted theorem interior_euclideanQuadrant

added theorem interior_quadrant

added theorem interior_range_modelWithCornersEuclideanQuadrant

added theorem modelWithCornersEuclideanQuadrant_zero

added theorem range_modelWithCornersEuclideanQuadrant