Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 20:11 0d473696

View on Github →

feat(topology/metric/hausdorff_distance): more properties of cthickening (#10808)

Estimated changes

Modified src/topology/metric_space/basic.lean

added theorem eventually_closed_ball_subset

added theorem metric.bounded_range_of_tendsto

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem is_compact.exists_inf_edist_eq_edist

added theorem metric.bounded.cthickening

added theorem metric.bounded.thickening

added theorem metric.mem_cthickening_of_dist_le

added theorem metric.mem_cthickening_of_edist_le