Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-24 21:14 c4268a86

View on Github →

feat(topology,analysis): there exists y ∈ frontier s at distance inf_dist x sᶜ from x (#10976)

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

added theorem exists_mem_frontier_inf_dist_compl_eq_dist

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem is_closed.exists_inf_dist_eq_dist

added theorem is_compact.exists_inf_dist_eq_dist

modified theorem is_compact.exists_inf_edist_eq_edist

added theorem metric.closed_ball_inf_dist_compl_subset_closure'

added theorem metric.closed_ball_inf_dist_compl_subset_closure

added theorem metric.disjoint_ball_inf_dist

added theorem metric.exists_mem_closure_inf_dist_eq_dist

added theorem metric.inf_dist_inter_closed_ball_of_mem

added theorem metric.not_mem_of_dist_lt_inf_dist