Finite basis with small vectors

Stream: Is there code for X?

[Yaël Dillies]

We have docs#finite_dimensional.fin_basis, but is there a definition for a finite basis where all vectors are small (all of length 1 would be fine by me)? Here is my context

import analysis.convex.topology

variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E]

[Yaël Dillies]

To un-#xy I am following the proof here, except that I restrict to a set, so for all x ∈ interior s I need to construct a ball containing x and a finite subset of s whose convex hull contains that ball.