Commit 2022-02-25 20:13 3cc9ac40

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.