Documentation Verification Report

GromovHausdorffRealized

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

Statistics

Metric	Count
Definitions `HD`, `OptimalGHCoupling`, `candidates`, `candidatesBDist`, `candidatesBOfCandidates`, `instMetricSpaceOptimalGHCoupling`, `optimalGHInjl`, `optimalGHInjr`, `premetricOptimalGHDist`	9
Theorems `HD_below_aux1`, `HD_below_aux2`, `HD_candidatesBDist_le`, `candidatesBDist_mem_candidatesB`, `candidatesBOfCandidates_mem`, `compactSpace_optimalGHCoupling`, `hausdorffDist_optimal_le_HD`, `isometry_optimalGHInjl`, `isometry_optimalGHInjr`	9
Total	18

GromovHausdorff

Definitions

Name	Category	Theorems
`HD` 📖	CompOp	2 math math: `hausdorffDist_optimal_le_HD`, `HD_candidatesBDist_le`
`OptimalGHCoupling` 📖	CompOp	5 math math: `hausdorffDist_optimal`, `isometry_optimalGHInjr`, `hausdorffDist_optimal_le_HD`, `compactSpace_optimalGHCoupling`, `isometry_optimalGHInjl`
`candidates` 📖	CompOp	—
`candidatesBDist` 📖	CompOp	2 math math: `candidatesBDist_mem_candidatesB`, `HD_candidatesBDist_le`
`candidatesBOfCandidates` 📖	CompOp	1 math math: `candidatesBOfCandidates_mem`
`instMetricSpaceOptimalGHCoupling` 📖	CompOp	5 math math: `hausdorffDist_optimal`, `isometry_optimalGHInjr`, `hausdorffDist_optimal_le_HD`, `compactSpace_optimalGHCoupling`, `isometry_optimalGHInjl`
`optimalGHInjl` 📖	CompOp	3 math math: `hausdorffDist_optimal`, `hausdorffDist_optimal_le_HD`, `isometry_optimalGHInjl`
`optimalGHInjr` 📖	CompOp	3 math math: `hausdorffDist_optimal`, `isometry_optimalGHInjr`, `hausdorffDist_optimal_le_HD`
`premetricOptimalGHDist` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`HD_below_aux1` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `Set.range` `Real.instAdd` `DFunLike.coe` `BoundedContinuousFunction.instFunLike` `instTopologicalSpaceProd` `instTopologicalSpaceSum` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Real.pseudoMetricSpace`	—	`Bornology.IsBounded.bddBelow` `Real.instIsOrderBornology` `BoundedContinuousFunction.isBounded_range` `Set.forall_mem_range` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.mem_range_self` `le_refl`
`HD_below_aux2` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `Set.range` `Real.instAdd` `DFunLike.coe` `BoundedContinuousFunction.instFunLike` `instTopologicalSpaceProd` `instTopologicalSpaceSum` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Real.pseudoMetricSpace`	—	`Bornology.IsBounded.bddBelow` `Real.instIsOrderBornology` `BoundedContinuousFunction.isBounded_range` `Set.forall_mem_range` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.mem_range_self` `le_refl`
`HD_candidatesBDist_le` 📖	mathematical	—	`Real` `Real.instLE` `HD` `candidatesBDist` `Real.instAdd` `Metric.diam` `MetricSpace.toPseudoMetricSpace` `Set.univ` `Real.instOne`	—	`max_le` `ciSup_le` `ciInf_le` `add_zero` `HD_below_aux1` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `add_le_add_left` `Metric.dist_le_diam_of_mem` `Metric.isBounded_of_compactSpace` `Set.mem_univ` `le_trans` `HD_below_aux2`
`candidatesBDist_mem_candidatesB` 📖	mathematical	—	`Set` `Set.instMembership` `candidatesBDist`	—	`candidatesBOfCandidates_mem`
`candidatesBOfCandidates_mem` 📖	mathematical	`Set` `Set.instMembership` `candidates`	`candidatesBOfCandidates`	—	—
`compactSpace_optimalGHCoupling` 📖	mathematical	—	`CompactSpace` `OptimalGHCoupling` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpaceOptimalGHCoupling`	—	`Set.range_quotient_mk'` `isCompact_range` `instCompactSpaceSum` `continuous_sum_dom` `Isometry.continuous` `isometry_optimalGHInjl` `isometry_optimalGHInjr`
`hausdorffDist_optimal_le_HD` 📖	mathematical	`Set` `Set.instMembership`	`Real` `Real.instLE` `Metric.hausdorffDist` `OptimalGHCoupling` `MetricSpace.toPseudoMetricSpace` `instMetricSpaceOptimalGHCoupling` `Set.range` `optimalGHInjl` `optimalGHInjr` `HD`	—	`le_trans` `le_of_forall_gt_imp_ge_of_dense` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_le_of_lt` `le_max_left` `le_csSup` `add_zero` `Set.mem_range_self` `exists_lt_of_csInf_lt` `Set.range_nonempty` `le_of_lt` `Metric.hausdorffDist_le_of_mem_dist` `dist_nonneg` `le_max_right` `dist_comm`
`isometry_optimalGHInjl` 📖	mathematical	—	`Isometry` `OptimalGHCoupling` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpaceOptimalGHCoupling` `optimalGHInjl`	—	`Isometry.of_dist_eq`
`isometry_optimalGHInjr` 📖	mathematical	—	`Isometry` `OptimalGHCoupling` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpaceOptimalGHCoupling` `optimalGHInjr`	—	`Isometry.of_dist_eq`

---

← Back to Index