Commit 2026-08-31 08:01 d00a6cc5

View on Github →

feat(Geometry/Euclidean): cross section perpendicular to the altitude of the simplex (#43054) Extracted from #37910. This sets up affine geometry lemma for calculating the volume. The leaf lemma in this PR is Affine.Simplex.closedInterior_inter_affineSubspaceMk'_lineMap_altitudeFoot, which says that {cross section parallel to the base} and {cross section perpendicular to the altitude} is the same

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

added theorem Submodule.comap_orthogonal

added theorem Submodule.comap_orthogonal_of_le

Modified Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

added theorem Submodule.orthogonal_inf_orthogonal_inf_of_le

Modified Mathlib/Geometry/Euclidean/Altitude.lean

added theorem Affine.Simplex.affineSubspaceMk'_lineMap_altitudeFoot_eq_shift

added theorem Affine.Simplex.closedInterior_inter_affineSubspaceMk'_lineMap_altitudeFoot

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

modified theorem AffineSubspace.coe_inf

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Shift.lean

added theorem AffineSubspace.lineMap_mem_shift

added theorem AffineSubspace.vadd_mem_shift