Mathlib v3 is deprecated. Go to Mathlib v4

Theorem interior_convex_hull_aff_basis

Modification history

2022-11-09 14:43
src/analysis/normed_space/add_torsor_bases.lean
refactor(linear_algebra,analysis/normed_space): use `finite`, review API, golf (#17320) …
Deleted interior_convex_hull_aff_basisView on Github →
2022-08-30 13:54
src/analysis/normed_space/add_torsor_bases.lean
chore(analysis, measure_theory): Fix lint (#16216) …
Modified interior_convex_hull_aff_basisView on Github →
2022-07-24 16:34
src/analysis/normed_space/add_torsor_bases.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified interior_convex_hull_aff_basisView on Github →
2021-10-07 06:55
src/analysis/normed_space/add_torsor_bases.lean
feat(analysis/normed_space/add_torsor_bases): the interior of the convex hull of a finite affine basis is the set of points with strictly positive barycentric coordinates (#9583) …
Added interior_convex_hull_aff_basisView on Github →