add_torsor_bases): add lemma `smooth_barycentric_coord` (#13764)

Commit

3 years ago

feat(analysis/normed_space/add_torsor_bases): add lemma `smooth_barycentric_coord` (#13764) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents