Theorem modelWithCornersEuclideanHalfSpace_symm_apply_of_le

Modification history

2026-08-10 13:55
Mathlib/Geometry/Manifold/Instances/Real.lean
chore: tweak API for modelWithCornersEuclideanHalfSpace (#42281) …
Added modelWithCornersEuclideanHalfSpace_symm_apply_of_leView on Github →