Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-11 00:47 590444c4

View on Github →

chore(topology/metric/hausdorff_distance): use infi/supr (#6611)

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.sup_eq_zero

added theorem ennreal.supr_eq_zero

Modified src/topology/instances/ennreal.lean

deleted theorem ennreal.supr_eq_zero

Modified src/topology/metric_space/hausdorff_distance.lean

modified def emetric.inf_edist

modified theorem emetric.inf_edist_empty

added theorem emetric.le_inf_edist