mathlib3
02a25602 - feat(analysis/normed_space/add_torsor_bases): add `convex.interior_nonempty_iff_affine_span_eq_top` (#13220)

Commit
3 years ago
feat(analysis/normed_space/add_torsor_bases): add `convex.interior_nonempty_iff_affine_span_eq_top` (#13220) Generalize `interior_convex_hull_nonempty_iff_aff_span_eq_top` to any convex set, not necessarily written as the convex hull of a set.
Author
Parents
Loading