Commit 2025-07-05 01:29 0f3d4626

View on Github →

feat(LinearAlgebra/AffineSpace/Independent): faceOpposite point in 1-simplex (#26527) Add a lemma about the point of faceOpposite applied to a 1-simplex.

lemma faceOpposite_point_eq_point_rev (s : Simplex k P 1) (i : Fin 2) (n : Fin 1) :
    (s.faceOpposite i).points n = s.points i.rev := by

Estimated changes

Modified Mathlib/Data/Finset/Sort.lean

added theorem Finset.orderEmbOfFin_compl_singleton

added theorem Finset.orderEmbOfFin_compl_singleton_apply

added theorem Finset.orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem Affine.Simplex.faceOpposite_point_eq_point_one

added theorem Affine.Simplex.faceOpposite_point_eq_point_rev

added theorem Affine.Simplex.faceOpposite_point_eq_point_succAbove

added theorem Affine.Simplex.faceOpposite_point_eq_point_zero