Theorem Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite

Modification history

2025-05-01 21:43
Mathlib/Geometry/Euclidean/Altitude.lean
feat(Geometry/Euclidean/Altitude): `altitudeFoot`, `height` (#24525) …
Added Affine.Simplex.altitudeFoot_mem_affineSpan_faceOppositeView on Github →