Mathlib Changelog
v3
Changelog
About
Github
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