mathlib3

65d8b84e - feat(tooplogy/metric_space/hausdorff_distance): add lemmas about `thickening` (#15641)

feat(tooplogy/metric_space/hausdorff_distance): add lemmas about `thickening` (#15641) * rename `emetric.exists_pos_forall_le_edist` -> `emetric.exists_pos_forall_lt_edist`; - don't assume that the compact set is nonempty; - provide an `nnreal` number instead of an `ennreal`; - claim strict inequality; * add `metric.thickening_mem_nhds_set` and `metric.cthickening_mem_nhds_set`; * move `is_compact.exists_thickening_subset_open` below the `cthickening` version, make it clear from the proof that the latter implies the former; * add `metric.has_basis_nhds_set_thickening` and `metric.has_basis_nhds_set_cthickening`; * add `continuous.tendsto_nhds_set`