Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 22:25 8fbf296d

View on Github →

feat(topology/metric_space/hausdorff_distance): Hausdorff distance

Estimated changes

Modified src/topology/basic.lean

added def topological_space.closeds

added def topological_space.nonempty_compacts

Modified src/topology/continuity.lean

added def nonempty_compacts.to_closeds

Modified src/topology/metric_space/cau_seq_filter.lean

added theorem ennreal.cauchy_seq_of_edist_le_half_pow

added theorem ennreal.edist_le_two_mul_half_pow

added theorem ennreal.half_pow_add_succ

added theorem ennreal.half_pow_mono

added theorem ennreal.half_pow_pos

added theorem ennreal.half_pow_tendsto_zero

added theorem sequentially_complete.B2_lim

added theorem sequentially_complete.B2_pos

deleted theorem sequentially_complete.FB_lim

deleted theorem sequentially_complete.FB_pos

deleted theorem sequentially_complete.F_lim

deleted theorem sequentially_complete.F_pos

Created src/topology/metric_space/closeds.lean

added theorem emetric.closeds.edist_eq

added theorem emetric.continuous_inf_edist_Hausdorff_edist

added theorem emetric.is_closed_subsets_of_is_closed

added theorem emetric.nonempty_compacts.is_closed_in_closeds

added theorem emetric.nonempty_compacts.to_closeds.uniform_embedding

added theorem metric.nonempty_compacts.dist_eq

added theorem metric.uniform_continuous_inf_dist_Hausdorff_dist

Created src/topology/metric_space/hausdorff_distance.lean

added def emetric.Hausdorff_edist

added theorem emetric.Hausdorff_edist_closure

added theorem emetric.Hausdorff_edist_closure₁

added theorem emetric.Hausdorff_edist_closure₂

added theorem emetric.Hausdorff_edist_comm

added theorem emetric.Hausdorff_edist_empty

added theorem emetric.Hausdorff_edist_image

added theorem emetric.Hausdorff_edist_le_ediam

added theorem emetric.Hausdorff_edist_le_of_inf_edist

added theorem emetric.Hausdorff_edist_le_of_mem_edist

added theorem emetric.Hausdorff_edist_self

added theorem emetric.Hausdorff_edist_self_closure

added theorem emetric.Hausdorff_edist_triangle

added theorem emetric.Hausdorff_edist_zero_iff_closure_eq_closure

added theorem emetric.Hausdorff_edist_zero_iff_eq_of_closed

added theorem emetric.continuous_inf_edist

added theorem emetric.exists_edist_lt_of_Hausdorff_edist_lt

added theorem emetric.exists_edist_lt_of_inf_edist_lt

added def emetric.inf_edist

added theorem emetric.inf_edist_closure

added theorem emetric.inf_edist_empty

added theorem emetric.inf_edist_image

added theorem emetric.inf_edist_le_Hausdorff_edist_of_mem

added theorem emetric.inf_edist_le_edist_of_mem

added theorem emetric.inf_edist_le_inf_edist_add_Hausdorff_edist

added theorem emetric.inf_edist_le_inf_edist_add_edist

added theorem emetric.inf_edist_le_inf_edist_of_subset

added theorem emetric.inf_edist_singleton

added theorem emetric.inf_edist_union

added theorem emetric.inf_edist_zero_of_mem

added theorem emetric.mem_closure_iff_inf_edist_zero

added theorem emetric.mem_iff_ind_edist_zero_of_closed

added theorem emetric.ne_empty_of_Hausdorff_edist_ne_top

added def metric.Hausdorff_dist

added theorem metric.Hausdorff_dist_closure

added theorem metric.Hausdorff_dist_closure₁

added theorem metric.Hausdorff_dist_closure₂

added theorem metric.Hausdorff_dist_comm

added theorem metric.Hausdorff_dist_empty'

added theorem metric.Hausdorff_dist_empty

added theorem metric.Hausdorff_dist_image

added theorem metric.Hausdorff_dist_le_diam

added theorem metric.Hausdorff_dist_le_of_inf_dist

added theorem metric.Hausdorff_dist_le_of_mem_dist

added theorem metric.Hausdorff_dist_nonneg

added theorem metric.Hausdorff_dist_self_closure

added theorem metric.Hausdorff_dist_self_zero

added theorem metric.Hausdorff_dist_triangle'

added theorem metric.Hausdorff_dist_triangle

added theorem metric.Hausdorff_dist_zero_iff_closure_eq_closure

added theorem metric.Hausdorff_dist_zero_iff_eq_of_closed

added theorem metric.Hausdorff_edist_ne_top_of_ne_empty_of_bounded

added theorem metric.continuous_inf_dist

added theorem metric.exists_dist_lt_of_Hausdorff_dist_lt'

added theorem metric.exists_dist_lt_of_Hausdorff_dist_lt

added theorem metric.exists_dist_lt_of_inf_dist_lt

added def metric.inf_dist

added theorem metric.inf_dist_empty

added theorem metric.inf_dist_eq_closure

added theorem metric.inf_dist_image

added theorem metric.inf_dist_le_Hausdorff_dist_of_mem

added theorem metric.inf_dist_le_dist_of_mem

added theorem metric.inf_dist_le_inf_dist_add_Hausdorff_dist

added theorem metric.inf_dist_le_inf_dist_add_dist

added theorem metric.inf_dist_le_inf_dist_of_subset

added theorem metric.inf_dist_nonneg

added theorem metric.inf_dist_singleton

added theorem metric.inf_dist_zero_of_mem

added theorem metric.inf_edist_ne_top

added theorem metric.mem_closure_iff_inf_dist_zero

added theorem metric.mem_iff_ind_dist_zero_of_closed

added theorem metric.uniform_continuous_inf_dist