Documentation Verification Report

GromovHausdorff

📁 Source: Mathlib/Topology/MetricSpace/GromovHausdorff.lean

Statistics

Metric	Count
Definitions `AuxGluingStruct`, `Space`, `embed`, `metric`, `GHSpace`, `setoid`, `auxGluing`, `ghDist`, `instDistGHSpace`, `instInhabitedAuxGluingStruct`, `instInhabitedGHSpace`, `instMetricSpaceGHSpace`, `repGHSpaceMetricSpace`, `toGHSpace`, `toGHSpace`	15
Theorems `isom`, `toGHSpace_rep`, `dist_ghDist`, `eq_toGHSpace`, `eq_toGHSpace_iff`, `ghDist_eq_hausdorffDist`, `ghDist_le_hausdorffDist`, `ghDist_le_nonemptyCompacts_dist`, `ghDist_le_of_approx_subsets`, `hausdorffDist_optimal`, `instCompleteSpaceGHSpace`, `instSecondCountableTopologyGHSpace`, `rep_gHSpace_compactSpace`, `rep_gHSpace_nonempty`, `toGHSpace_continuous`, `toGHSpace_eq_toGHSpace_iff_isometryEquiv`, `toGHSpace_lipschitz`, `totallyBounded`	18
Total	33

GromovHausdorff

Definitions

Name	Category	Theorems
`AuxGluingStruct` 📖	CompData	—
`GHSpace` 📖	CompOp	7 math math: `dist_ghDist`, `totallyBounded`, `toGHSpace_continuous`, `instCompleteSpaceGHSpace`, `ghDist_le_nonemptyCompacts_dist`, `instSecondCountableTopologyGHSpace`, `toGHSpace_lipschitz`
`auxGluing` 📖	CompOp	—
`ghDist` 📖	CompOp	5 math math: `hausdorffDist_optimal`, `dist_ghDist`, `ghDist_le_hausdorffDist`, `ghDist_eq_hausdorffDist`, `ghDist_le_of_approx_subsets`
`instDistGHSpace` 📖	CompOp	2 math math: `dist_ghDist`, `ghDist_le_nonemptyCompacts_dist`
`instInhabitedAuxGluingStruct` 📖	CompOp	—
`instInhabitedGHSpace` 📖	CompOp	—
`instMetricSpaceGHSpace` 📖	CompOp	5 math math: `totallyBounded`, `toGHSpace_continuous`, `instCompleteSpaceGHSpace`, `instSecondCountableTopologyGHSpace`, `toGHSpace_lipschitz`
`repGHSpaceMetricSpace` 📖	CompOp	3 math math: `dist_ghDist`, `rep_gHSpace_compactSpace`, `GHSpace.toGHSpace_rep`
`toGHSpace` 📖	CompOp	4 math math: `toGHSpace_eq_toGHSpace_iff_isometryEquiv`, `eq_toGHSpace`, `GHSpace.toGHSpace_rep`, `eq_toGHSpace_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_ghDist` 📖	mathematical	—	`Dist.dist` `GHSpace` `instDistGHSpace` `ghDist` `GHSpace.Rep` `repGHSpaceMetricSpace` `rep_gHSpace_nonempty` `rep_gHSpace_compactSpace`	—	`rep_gHSpace_nonempty` `rep_gHSpace_compactSpace` `ghDist.eq_1` `GHSpace.toGHSpace_rep`
`eq_toGHSpace` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `PreLp` `Real` `Real.normedAddCommGroup` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `lp.inftyNormedCommRing` `Real.normedCommRing` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `Real.normedField` `IsometryRel.setoid` `toGHSpace` `TopologicalSpace.NonemptyCompacts.instSetLike` `Subtype.metricSpace` `NormedRing.toMetricSpace` `lp.inftyNormedRing` `NormedCommRing.toNormedRing` `TopologicalSpace.NonemptyCompacts.toCompactSpace` `TopologicalSpace.NonemptyCompacts.toNonempty`	—	`NormedDivisionRing.to_normOneClass` `TopologicalSpace.NonemptyCompacts.toCompactSpace` `TopologicalSpace.NonemptyCompacts.toNonempty` `eq_toGHSpace_iff` `isometry_subtype_coe` `Subtype.range_coe`
`eq_toGHSpace_iff` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `PreLp` `Real` `Real.normedAddCommGroup` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `lp.inftyNormedCommRing` `Real.normedCommRing` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `Real.normedField` `IsometryRel.setoid` `toGHSpace` `Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedRing.toMetricSpace` `lp.inftyNormedRing` `NormedCommRing.toNormedRing` `Set.range` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike`	—	`NormedDivisionRing.to_normOneClass` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `kuratowskiEmbedding.isometry` `Isometry.comp` `isometry_subtype_coe` `IsometryEquiv.isometry` `Set.range_comp'` `IsometryEquiv.range_eq_univ` `Set.image_univ` `Subtype.range_coe`
`ghDist_eq_hausdorffDist` 📖	mathematical	—	`Isometry` `PreLp` `Real` `Real.normedAddCommGroup` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedRing.toMetricSpace` `lp.inftyNormedRing` `NormedCommRing.toNormedRing` `Real.normedCommRing` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `Real.normedField` `ghDist` `Metric.hausdorffDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `lp.inftyNormedCommRing` `Set.range`	—	`TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `compactSpace_optimalGHCoupling` `PseudoEMetricSpace.pseudoMetrizableSpace` `NormedDivisionRing.to_normOneClass` `Isometry.comp` `kuratowskiEmbedding.isometry` `isometry_optimalGHInjl` `isometry_optimalGHInjr` `Set.image_univ` `Set.image_comp` `hausdorffDist_optimal` `Metric.hausdorffDist_image`
`ghDist_le_hausdorffDist` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`Real` `Real.instLE` `ghDist` `Metric.hausdorffDist` `MetricSpace.toPseudoMetricSpace` `Set.range`	—	`Set.exists_mem_of_nonempty` `Set.mem_union_left` `Set.mem_range_self` `Set.mem_union_right` `IsCompact.union` `isCompact_range` `Isometry.continuous` `isCompact_iff_isCompact_univ` `Set.range_comp` `Metric.hausdorffDist_image` `isometry_subtype_coe` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `NormedDivisionRing.to_normOneClass` `kuratowskiEmbedding.isometry` `IsCompact.image` `Set.Nonempty.image` `Set.range_nonempty` `eq_toGHSpace_iff` `Isometry.comp` `KuratowskiEmbedding.exists_isometric_embedding` `csInf_le` `Metric.hausdorffDist_nonneg` `Set.mem_image`
`ghDist_le_nonemptyCompacts_dist` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `GHSpace` `instDistGHSpace` `TopologicalSpace.NonemptyCompacts.toGHSpace` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `PseudoMetricSpace.toDist` `Metric.NonemptyCompacts.instMetricSpace`	—	`isometry_subtype_coe` `Subtype.range_coe_subtype` `ghDist_le_hausdorffDist`
`ghDist_le_of_approx_subsets` 📖	mathematical	`Set` `Set.instMembership` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Set.Elem` `Subtype.pseudoMetricSpace`	`ghDist` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`le_of_forall_pos_le_add` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `Set.exists_mem_of_nonempty` `Set.Nonempty.to_subtype` `le_trans` `abs_nonneg` `covariant_swap_add_of_covariant_add` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `CancelDenoms.add_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `lt_of_not_ge` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.mul_nonpos` `Isometry.of_dist_eq` `ghDist_le_hausdorffDist` `IsCompact.isBounded` `isCompact_range` `Isometry.continuous` `Metric.hausdorffDist_triangle` `Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded` `Set.range_nonempty` `Set.Nonempty.image` `Bornology.IsBounded.subset` `Set.image_subset_range` `Metric.hausdorffDist_triangle'` `Set.image_univ` `Metric.hausdorffDist_image` `dist_nonneg` `Metric.hausdorffDist_le_of_mem_dist` `Set.mem_univ` `dist_self` `Set.mem_image` `Set.mem_image_of_mem` `Set.mem_range_self` `le_of_eq` `Metric.glueDist_glued_points` `Set.mem_range` `dist_comm` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.add_nonpos`
`hausdorffDist_optimal` 📖	mathematical	—	`Metric.hausdorffDist` `OptimalGHCoupling` `MetricSpace.toPseudoMetricSpace` `instMetricSpaceOptimalGHCoupling` `Set.range` `optimalGHInjl` `optimalGHInjr` `ghDist`	—	`NormedDivisionRing.to_normOneClass` `eq_toGHSpace_iff` `Nat.instAtLeastTwoHAddOfNat` `Set.exists_mem_of_nonempty` `Set.mem_range_self` `Metric.exists_dist_lt_of_hausdorffDist_lt` `Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded` `TopologicalSpace.NonemptyCompacts.nonempty` `IsCompact.isBounded` `TopologicalSpace.NonemptyCompacts.isCompact` `Set.mem_range` `Isometry.diam_range` `Metric.diam_union` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_le_add_right` `le_of_lt` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Isometry.dist_eq` `dist_comm` `dist_triangle` `Set.mem_union_left` `Set.mem_union_right` `Metric.dist_le_diam_of_mem` `hausdorffDist_optimal_le_HD` `candidatesBOfCandidates_mem` `le_trans` `le_of_forall_gt_imp_ge_of_dense` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ciInf_le` `add_zero` `HD_below_aux1` `Metric.exists_dist_lt_of_hausdorffDist_lt'` `HD_below_aux2` `ciSup_le` `candidatesBDist_mem_candidatesB` `HD_candidatesBDist_le` `not_lt` `le_antisymm` `le_csInf` `Set.Nonempty.image` `Set.Nonempty.prod` `ghDist_le_hausdorffDist` `isometry_optimalGHInjl` `isometry_optimalGHInjr`
`instCompleteSpaceGHSpace` 📖	mathematical	—	`CompleteSpace` `GHSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpaceGHSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `Metric.complete_of_convergent_controlled_sequences` `rep_gHSpace_compactSpace` `rep_gHSpace_nonempty` `AuxGluingStruct.isom` `isometry_optimalGHInjl` `Isometry.comp` `Metric.toGlueL_isometry` `UniformSpace.Completion.coe_isometry` `Metric.toInductiveLimit_isometry` `Metric.toInductiveLimit_commute` `Set.range_comp` `Metric.hausdorffDist_image` `Metric.toGlueR_isometry` `hausdorffDist_optimal` `dist_ghDist` `le_refl` `isCompact_range` `Isometry.continuous` `Set.range_nonempty` `cauchySeq_of_le_geometric` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `one_mul` `le_of_lt` `cauchySeq_tendsto_of_complete` `TopologicalSpace.NonemptyCompacts.instCompleteSpace` `UniformSpace.Completion.completeSpace` `TopologicalSpace.NonemptyCompacts.toGHSpace.eq_1` `GHSpace.toGHSpace_rep` `toGHSpace_eq_toGHSpace_iff_isometryEquiv` `Filter.Tendsto.congr` `Filter.Tendsto.comp` `Continuous.tendsto` `toGHSpace_continuous`
`instSecondCountableTopologyGHSpace` 📖	mathematical	—	`SecondCountableTopology` `GHSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpaceGHSpace`	—	`Metric.secondCountable_of_countable_discretization` `Nat.instAtLeastTwoHAddOfNat` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.instIsOrderedRing` `Real.instNontrivial` `finite_cover_balls_of_compact` `isCompact_univ` `rep_gHSpace_compactSpace` `rep_gHSpace_nonempty` `ghDist_le_of_approx_subsets` `Set.mem_univ` `Set.mem_iUnion₂` `LT.lt.le` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply` `Fin.heq_fun₂_iff` `abs_mul` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_pos` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsInt.to_isRat` `le_of_lt` `Int.abs_sub_lt_one_of_floor_eq_floor` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `div_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `mul_one` `dist_ghDist` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat`
`rep_gHSpace_compactSpace` 📖	mathematical	—	`CompactSpace` `GHSpace.Rep` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `repGHSpaceMetricSpace`	—	`NormedDivisionRing.to_normOneClass` `TopologicalSpace.NonemptyCompacts.toCompactSpace`
`rep_gHSpace_nonempty` 📖	mathematical	—	`GHSpace.Rep`	—	`TopologicalSpace.NonemptyCompacts.toNonempty`
`toGHSpace_continuous` 📖	mathematical	—	`Continuous` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `GHSpace` `TopologicalSpace.NonemptyCompacts.topology` `instMetricSpaceGHSpace` `TopologicalSpace.NonemptyCompacts.toGHSpace`	—	`LipschitzWith.continuous` `toGHSpace_lipschitz`
`toGHSpace_eq_toGHSpace_iff_isometryEquiv` 📖	mathematical	—	`toGHSpace` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	—	`Quotient.eq` `NormedDivisionRing.to_normOneClass` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `kuratowskiEmbedding.isometry`
`toGHSpace_lipschitz` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `GHSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpaceGHSpace` `NNReal` `instOneNNReal` `TopologicalSpace.NonemptyCompacts.toGHSpace`	—	`LipschitzWith.mk_one` `ghDist_le_nonemptyCompacts_dist`
`totallyBounded` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLE` `Metric.diam` `GHSpace.Rep` `MetricSpace.toPseudoMetricSpace` `repGHSpaceMetricSpace` `Set.univ` `Cardinal` `Cardinal.instLE` `Set.Elem` `Cardinal.instNatCast` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `Metric.ball`	`TotallyBounded` `GHSpace` `instMetricSpaceGHSpace`	—	`Metric.totallyBounded_of_finite_discretization` `Nat.instAtLeastTwoHAddOfNat` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.instIsOrderedRing` `Real.instNontrivial` `Metric.tendsto_atTop` `le_rfl` `le_of_lt` `lt_of_le_of_lt` `le_abs_self` `sub_eq_add_neg` `neg_zero` `add_zero` `Fintype.card_eq` `Set.card_empty` `Fintype.card_fin` `bot_le` `Set.not_notMem` `Cardinal.lt_aleph0` `LE.le.trans_lt` `Cardinal.natCast_lt_aleph0` `Cardinal.mk_fin` `Nat.cast_le` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `min_le_left` `rep_gHSpace_nonempty` `rep_gHSpace_compactSpace` `ghDist_le_of_approx_subsets` `Set.mem_univ` `Set.mem_iUnion₂` `le_trans` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply` `min_eq_right` `Nat.floor_mono` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `LE.le.trans` `Metric.dist_le_diam_of_mem` `IsCompact.isBounded` `isCompact_univ` `le_max_left` `LT.lt.le` `inv_pos` `Fin.heq_fun₂_iff` `Int.floor_nonneg` `mul_nonneg` `dist_nonneg` `Int.floor_toNat` `abs_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Int.abs_sub_lt_one_of_floor_eq_floor` `mul_inv_cancel₀` `ne_of_gt` `one_mul` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_assoc` `mul_one` `dist_ghDist` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNNRat_add` `half_lt_self`

GromovHausdorff.AuxGluingStruct

Definitions

Name	Category	Theorems
`Space` 📖	CompOp	1 math math: `isom`
`embed` 📖	CompOp	1 math math: `isom`
`metric` 📖	CompOp	1 math math: `isom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isom` 📖	mathematical	—	`Isometry` `Space` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metric` `embed`	—	—

GromovHausdorff.GHSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toGHSpace_rep` 📖	mathematical	—	`GromovHausdorff.toGHSpace` `Rep` `GromovHausdorff.repGHSpaceMetricSpace` `GromovHausdorff.rep_gHSpace_compactSpace` `GromovHausdorff.rep_gHSpace_nonempty`	—	`GromovHausdorff.rep_gHSpace_compactSpace` `GromovHausdorff.rep_gHSpace_nonempty` `NormedDivisionRing.to_normOneClass` `TopologicalSpace.NonemptyCompacts.toCompactSpace` `TopologicalSpace.NonemptyCompacts.toNonempty` `GromovHausdorff.eq_toGHSpace` `Quot.out_eq`

GromovHausdorff.IsometryRel

Definitions

Name	Category	Theorems
`setoid` 📖	CompOp	2 math math: `GromovHausdorff.eq_toGHSpace`, `GromovHausdorff.eq_toGHSpace_iff`

TopologicalSpace.NonemptyCompacts

Definitions

Name	Category	Theorems
`toGHSpace` 📖	CompOp	3 math math: `GromovHausdorff.toGHSpace_continuous`, `GromovHausdorff.ghDist_le_nonemptyCompacts_dist`, `GromovHausdorff.toGHSpace_lipschitz`

---

← Back to Index