Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-23 10:19
223cb8de
View on Github →
feat: Intercalate a simplex between a point and a neighborhood (
#14660
) ... in finite dimensions.
Estimated changes
Modified
Mathlib/Analysis/Convex/Normed.lean
added
theorem
exists_mem_interior_convexHull_affineBasis