Theorem stdSimplex_unique

Modification history

2025-08-29 09:05
Mathlib/Analysis/Convex/Basic.lean
chore(Analysis/Convex): move to new file StdSimplex (#29097) …
Modified stdSimplex_uniqueView on Github →
2025-04-28 14:59
Mathlib/Analysis/Convex/Basic.lean
chore(Analysis/Convex): drop unused arguments (#24392) …
Modified stdSimplex_uniqueView on Github →
2024-10-12 06:38
Mathlib/Analysis/Convex/Basic.lean
chore(*): assume `[Nonempty α] [Subsingleton α]` instead of `Unique α` (#17670)
Modified stdSimplex_uniqueView on Github →
2024-02-08 13:29
Mathlib/Analysis/Convex/Basic.lean
feat(Analysis/Convex): lemmas about low-dimensional `stdSimplex`es (#10325) …
Added stdSimplex_uniqueView on Github →