Theorem Affine.Simplex.altitude_restrict_eq_comap_subtype

Modification history

2026-01-21 00:52
Mathlib/Geometry/Euclidean/Altitude.lean
feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas (#32021) …
Added Affine.Simplex.altitude_restrict_eq_comap_subtypeView on Github →