Commit 2022-07-26 11:31 65d8b84e

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