add_torsor_bases): add lemma `exists_subset_affine_independent_span_eq_top_of_open` (#9418)

Commit

4 years ago

feat(analysis/normed_space/add_torsor_bases): add lemma `exists_subset_affine_independent_span_eq_top_of_open` (#9418) Also some supporting lemmas about affine span, affine independence.

Author

ocfnash

Parents

931cd6d7

mathlib a24b4965 - feat(analysis/normed_space/add_torsor_bases): add lemma `exists_subset_affine_independent_span_eq_top_of_open` (#9418)

mathlib
a24b4965 - feat(analysis/normed_space/add_torsor_bases): add lemma `exists_subset_affine_independent_span_eq_top_of_open` (#9418)