Theorem modelWithCornersEuclideanHalfSpace_apply

Modification history

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