Commit 2025-09-21 16:51 b5990791

View on Github →

feat(Analysis/Convex/Between): interior of a 1-simplex (#29418) Add lemmas relating the interior or closedInterior of a 1-simplex to betweenness.

Estimated changes

Modified Mathlib/Analysis/Convex/Between.lean

added theorem Affine.Simplex.closedInterior_eq_affineSegment

added theorem Affine.Simplex.closedInterior_face_eq_affineSegment

added theorem Affine.Simplex.interior_eq_image_Ioo

added theorem Affine.Simplex.mem_closedInterior_face_iff_wbtw

added theorem Affine.Simplex.mem_closedInterior_iff_wbtw

added theorem Affine.Simplex.mem_interior_face_iff_sbtw

added theorem Affine.Simplex.mem_interior_iff_sbtw