mathlib3

3cc9ac40 - feat(analysis/normed_space/finite_dimension): add a lemma about `inf_dist` (#12282)

feat(analysis/normed_space/finite_dimension): add a lemma about `inf_dist` (#12282) Add a version of `exists_mem_frontier_inf_dist_compl_eq_dist` for a compact set in a real normed space. This version does not assume that the ambient space is finite dimensional.