feat(analysis/normed_space/add_torsor_bases): add `convex.interior_no…

…nempty_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.

src/analysis/normed_space/add_torsor_bases.lean

@@ -151,3 +151,7 @@ begin
       (finset.sum_centroid_weights_eq_one_of_nonempty ℝ (finset.univ : finset t) htne),
       finset.centroid_weights_apply, nat.cast_pos, inv_pos, finset.card_pos.mpr htne], },
 end
+
+lemma convex.interior_nonempty_iff_affine_span_eq_top [finite_dimensional ℝ V] {s : set V}
+  (hs : convex ℝ s) : (interior s).nonempty ↔ affine_span ℝ s = ⊤ :=
+by rw [← interior_convex_hull_nonempty_iff_aff_span_eq_top, hs.convex_hull_eq]