Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.inf_dist_zero_of_mem_closure

Modification history

2022-02-25 20:13
src/topology/metric_space/hausdorff_distance.lean
feat(analysis/normed_space/finite_dimension): add a lemma about `inf_dist` (#12282) …
Added metric.inf_dist_zero_of_mem_closureView on Github →