Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 18:15 2e83d617

View on Github →

feat(topology/metric_space/hausdorff_distance): Thickening the closure (#13515) thickening δ (closure s) = thickening δ s and other simple lemmas. Also rename inf_edist_le_inf_edist_of_subset to inf_edist_anti and make arguments to mem_thickening_iff implicit.

Estimated changes

Modified src/data/real/ennreal.lean

Modified src/data/set/lattice.lean

added theorem infi_Union

added theorem supr_Union

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem emetric.inf_edist_Union

added theorem emetric.inf_edist_anti

added theorem emetric.inf_edist_le_edist_add_inf_edist

deleted theorem emetric.inf_edist_le_inf_edist_of_subset

added theorem metric.cthickening_closure

added theorem metric.cthickening_union

added theorem metric.inf_edist_le_inf_edist_cthickening_add

added theorem metric.inf_edist_le_inf_edist_thickening_add

added theorem metric.mem_cthickening_iff

modified theorem metric.mem_thickening_iff

added theorem metric.mem_thickening_iff_inf_edist_lt

added theorem metric.thickening_Union

added theorem metric.thickening_closure

added theorem metric.thickening_of_nonpos

added theorem metric.thickening_union