Commit 2023-06-05 13:56 92923b36

View on Github →

feat: port Geometry.Manifold.Instances.Real (#4654)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

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

added theorem EuclideanHalfSpace.ext

added def EuclideanHalfSpace

added theorem EuclideanQuadrant.ext

added def EuclideanQuadrant

added def IccLeftChart

added def IccRightChart

added def modelWithCornersEuclideanHalfSpace

added def modelWithCornersEuclideanQuadrant

added theorem range_half_space

added theorem range_quadrant