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) …
Modified metric.closed_ball_inf_dist_compl_subset_closureView on Github →