Commit 2024-02-08 13:29 3939e04d

View on Github →

feat(Analysis/Convex): lemmas about low-dimensional stdSimplexes (#10325) Forward-port of leanprover-community/mathlib#19101 Motivated by https://github.com/Shamrock-Frost/BrouwerFixedPoint

Estimated changes

Modified Mathlib/Analysis/Convex/Basic.lean

modified theorem ite_eq_mem_stdSimplex

added theorem segment_single_subset_stdSimplex

added theorem single_mem_stdSimplex

added def stdSimplexEquivIcc

added theorem stdSimplex_fin_two

added theorem stdSimplex_of_isEmpty_index

added theorem stdSimplex_of_subsingleton

added theorem stdSimplex_unique

Modified Mathlib/Analysis/Convex/Topology.lean

added def stdSimplexHomeomorphUnitInterval