Theorem EuclideanHalfSpace.convex

Modification history

2024-12-09 10:07

Mathlib/Geometry/Manifold/Instances/Real.lean

feat(Geometry/Manifold): manifolds are locally path-connected (#17142) …

Added EuclideanHalfSpace.convex View on Github →