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)

Commit

4 years ago

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) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

a7784aad

mathlib cc46f314 - 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)

mathlib
cc46f314 - 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)