Theorem metric.closed_ball_inf_dist_compl_subset_closure'
Modification history
2022-03-28 06:13
src/analysis/normed_space/riesz_lemma.lean
feat(analysis/normed_space): generalize some lemmas (#12959) …
Deleted metric.closed_ball_inf_dist_compl_subset_closure'View on Github →