Commit 2022-03-17 17:30 a1bdaddf

View on Github →

chore(topology/metric_space/hausdorff_distance): move two lemmas (#12771) Remove the dependence of topology/metric_space/hausdorff_distance on analysis.normed_space.basic, by moving out two lemmas.

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/riesz_lemma.lean

added theorem metric.closed_ball_inf_dist_compl_subset_closure'

added theorem metric.closed_ball_inf_dist_compl_subset_closure

Modified src/topology/metric_space/hausdorff_distance.lean

deleted theorem metric.closed_ball_inf_dist_compl_subset_closure'

deleted theorem metric.closed_ball_inf_dist_compl_subset_closure

Modified src/topology/metric_space/pi_nat.lean

Modified src/topology/metric_space/polish.lean