Theorem stdSimplex_of_subsingleton

Modification history

2026-09-02 11:46
Mathlib/Analysis/Convex/StdSimplex.lean
refactor(AlgebraicTopology): redefine the topological simplex using `StdSimplex` instead of `stdSimplex` (#42181) …
Modified stdSimplex_of_subsingletonView on Github →
2025-08-29 09:05
Mathlib/Analysis/Convex/Basic.lean
chore(Analysis/Convex): move to new file StdSimplex (#29097) …
Modified stdSimplex_of_subsingletonView on Github →
2024-02-08 13:29
Mathlib/Analysis/Convex/Basic.lean
feat(Analysis/Convex): lemmas about low-dimensional `stdSimplex`es (#10325) …
Added stdSimplex_of_subsingletonView on Github →