Commit 2025-09-02 06:26 d4b26c77

View on Github →

feat(LinearAlgebra/AffineSpace/Simplex/Basic): membership of interior of a face (#27573) Add lemmas about when an affine combination of all the vertices of a simplex lies in the interior or closedInterior of a face. Feel free to golf, these lemmas really ought to be a lot simpler to prove.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq

added theorem AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype

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

added theorem Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc

added theorem Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg

added theorem Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo

added theorem Affine.Simplex.affineCombination_mem_interior_face_iff_pos

added theorem Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem

added theorem Affine.Simplex.affineCombination_mem_setInterior_iff

added theorem Affine.Simplex.setInterior_mono

added theorem Affine.Simplex.setInterior_subset_affineSpan