Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-07 23:05 4fecb101

View on Github →

feat(topology/gromov_hausdorff): the Gromov-Hausdorff space (#883)

Estimated changes

Created src/topology/metric_space/gromov_hausdorff.lean

added def Gromov_Hausdorff.GH_dist

added theorem Gromov_Hausdorff.GH_dist_eq_Hausdorff_dist

added theorem Gromov_Hausdorff.GH_dist_le_Hausdorff_dist

added theorem Gromov_Hausdorff.GH_dist_le_nonempty_compacts_dist

added theorem Gromov_Hausdorff.GH_dist_le_of_approx_subsets

added theorem Gromov_Hausdorff.GH_space.to_GH_space_rep

added theorem Gromov_Hausdorff.Hausdorff_dist_optimal

added def Gromov_Hausdorff.aux_gluing

added structure Gromov_Hausdorff.aux_gluing_struct

added theorem Gromov_Hausdorff.dist_GH_dist

added theorem Gromov_Hausdorff.eq_to_GH_space

added theorem Gromov_Hausdorff.eq_to_GH_space_iff

added theorem Gromov_Hausdorff.second_countable

added theorem Gromov_Hausdorff.to_GH_space_continuous

added theorem Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometric

added theorem Gromov_Hausdorff.to_GH_space_lipschitz

added theorem Gromov_Hausdorff.totally_bounded

Created src/topology/metric_space/gromov_hausdorff_realized.lean

added def Gromov_Hausdorff.HD

added theorem Gromov_Hausdorff.HD_below_aux1

added theorem Gromov_Hausdorff.HD_below_aux2

added theorem Gromov_Hausdorff.HD_candidates_b_dist_le

added theorem Gromov_Hausdorff.Hausdorff_dist_optimal_le_HD

added def Gromov_Hausdorff.candidates

added def Gromov_Hausdorff.candidates_b_dist

added theorem Gromov_Hausdorff.candidates_b_dist_mem_candidates_b

added def Gromov_Hausdorff.candidates_b_of_candidates

added theorem Gromov_Hausdorff.candidates_b_of_candidates_mem

added theorem Gromov_Hausdorff.isometry_optimal_GH_injl

added theorem Gromov_Hausdorff.isometry_optimal_GH_injr

added def Gromov_Hausdorff.optimal_GH_injl

added def Gromov_Hausdorff.optimal_GH_injr

added def Gromov_Hausdorff.premetric_optimal_GH_dist

Modified src/topology/metric_space/isometry.lean

added def Kuratowski_embedding.Kuratowski_embedding

added theorem Kuratowski_embedding.Kuratowski_embedding_isometry

added def Kuratowski_embedding.embedding_of_subset

added theorem Kuratowski_embedding.embedding_of_subset_coe

added theorem Kuratowski_embedding.embedding_of_subset_dist_le

added theorem Kuratowski_embedding.embedding_of_subset_isometry

added theorem Kuratowski_embedding.exists_isometric_embedding

added def Kuratowski_embedding.nonempty_compacts.Kuratowski_embedding

added def Kuratowski_embedding.ℓ_infty_ℝ