Commit 2024-04-06 14:26 39ba55a7

View on Github →

chore(Geometry/Manifold): rename two lemmas using mathlib3 names (#11929)

range_half_space -> range_euclideanHalfSpace
range_quadrant -> range_euclideanQuadrant

Estimated changes

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

added theorem range_euclideanHalfSpace

added theorem range_euclideanQuadrant

deleted theorem range_half_space

deleted theorem range_quadrant