Commit 2026-04-27 14:17 17f0cf84

View on Github →

feat(LinearAlgebra/Simplex): lemma for subset/disjoint relation between interior of simplex and its faces (#35365) Intermediate lemma towards #34826. This will be used to show the measure on interior and closedInterior are equal, as the difference is a zero-measure set.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean

added theorem Affine.Simplex.closedInterior_diff_interior

added theorem Affine.Simplex.closedInterior_eq_interior_union

added theorem Affine.Simplex.closedInterior_faceOpposite_ssubset_closedInterior

added theorem Affine.Simplex.closedInterior_faceOpposite_subset_closedInterior

added theorem Affine.Simplex.closedInterior_face_ssubset_closedInterior

added theorem Affine.Simplex.closedInterior_face_subset_closedInterior

added theorem Affine.Simplex.disjoint_interior_closedInterior_face

added theorem Affine.Simplex.disjoint_interior_closedInterior_faceOpposite

added theorem Affine.Simplex.point_mem_closedInterior_faceOpposite_iff

added theorem Affine.Simplex.point_mem_closedInterior_face_iff