Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 00:14 303e77c8

View on Github →

feat(topology/metric_space/hausdorff_distance): make iffs (#11288)

Make exists_edist_lt_of_inf_edist_lt and exists_dist_lt_of_inf_edist_lt iffs. Rename to inf_[e]dist_lt_iff.
Simplify some proofs

Estimated changes

Modified src/analysis/normed_space/riesz_lemma.lean

Modified src/measure_theory/measure/hausdorff.lean

Modified src/topology/metric_space/hausdorff_distance.lean

deleted theorem emetric.exists_edist_lt_of_inf_edist_lt

added theorem emetric.inf_edist_lt_iff

deleted theorem metric.exists_dist_lt_of_inf_dist_lt

added theorem metric.inf_dist_lt_iff