Documentation Verification Report

Completion

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

Statistics

Metric	Count
Definitions `extensionHom`, `instDist`, `instMetricSpace`	3
Theorems `completion_extension`, `completion_map`, `extensionHom_coe`, `completion_extension`, `completion_map`, `coe_isometry`, `continuous_dist`, `dist_comm`, `dist_eq`, `dist_self`, `dist_triangle`, `edist_eq`, `instIsBoundedSMul`, `mem_uniformity_dist`, `uniformContinuous_dist`, `uniformity_dist`, `uniformity_dist'`	17
Total	20

Isometry

Definitions

Name	Category	Theorems
`extensionHom` 📖	CompOp	5 math math: `extensionHom_coe`, `AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp`, `AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp`, `AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp`, `AbsoluteValue.Completion.extensionEmbedding_of_comp_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completion_extension` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `UniformSpace.Completion.instMetricSpace` `UniformSpace.Completion.extension`	—	`of_dist_eq` `UniformSpace.Completion.induction_on₂` `isClosed_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace` `T3Space.toT0Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `instOrderTopologyReal` `UniformSpace.pseudoMetrizableSpace` `EMetric.instIsCountablyGeneratedUniformity` `Continuous.dist` `Continuous.comp'` `UniformSpace.Completion.continuous_extension` `Continuous.fst` `continuous_id'` `Continuous.snd` `UniformSpace.Completion.extension_coe` `uniformContinuous` `dist_eq` `UniformSpace.Completion.dist_eq`
`completion_map` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `UniformSpace.Completion.instMetricSpace` `UniformSpace.Completion.map`	—	`completion_extension` `UniformSpace.Completion.completeSpace` `UniformSpace.Completion.t0Space` `comp` `UniformSpace.Completion.coe_isometry`
`extensionHom_coe` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `UniformSpace.Completion.ring` `extensionHom` `UniformSpace.Completion.coe'`	—	`UniformSpace.Completion.extensionHom_coe` `continuous`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completion_extension` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `UniformSpace.Completion.instMetricSpace` `UniformSpace.Completion.extension` `MetricSpace.toPseudoMetricSpace`	—	`of_dist_le_mul` `UniformSpace.Completion.induction_on₂` `isClosed_le` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Continuous.dist` `Continuous.comp'` `UniformSpace.Completion.continuous_extension` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_const` `UniformSpace.Completion.extension_coe` `MetricSpace.instT0Space` `uniformContinuous` `UniformSpace.Completion.dist_eq` `dist_le_mul`
`completion_map` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `UniformSpace.Completion.instMetricSpace` `UniformSpace.Completion.map`	—	`completion_extension` `UniformSpace.Completion.completeSpace` `comp` `Isometry.lipschitz` `UniformSpace.Completion.coe_isometry` `one_mul`

UniformSpace.Completion

Definitions

Name	Category	Theorems
`instDist` 📖	CompOp	9 math math: `uniformContinuous_dist`, `dist_eq`, `uniformity_dist`, `dist_comm`, `dist_triangle`, `AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp`, `uniformity_dist'`, `dist_self`, `continuous_dist`
`instMetricSpace` 📖	CompOp	11 math math: `NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal`, `LipschitzWith.completion_extension`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbedding`, `Isometry.completion_map`, `coe_isometry`, `Isometry.completion_extension`, `LipschitzWith.completion_map`, `AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal`, `instIsBoundedSMul`, `edist_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_isometry` 📖	mathematical	—	`Isometry` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpace` `coe'`	—	`Isometry.of_dist_eq` `dist_eq`
`continuous_dist` 📖	mathematical	`Continuous` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `UniformSpace.toTopologicalSpace` `uniformSpace`	`Real` `Real.pseudoMetricSpace` `Dist.dist` `instDist`	—	`Continuous.comp` `UniformContinuous.continuous` `uniformContinuous_dist` `Continuous.prodMk`
`dist_comm` 📖	mathematical	—	`Dist.dist` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `instDist`	—	`induction_on₂` `isClosed_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace` `T3Space.toT0Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `instOrderTopologyReal` `UniformSpace.pseudoMetrizableSpace` `EMetric.instIsCountablyGeneratedUniformity` `continuous_dist` `continuous_fst` `continuous_snd` `dist_eq` `dist_comm`
`dist_eq` 📖	mathematical	—	`Dist.dist` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `instDist` `coe'` `PseudoMetricSpace.toDist`	—	`extension₂_coe_coe` `T3Space.toT0Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `instOrderTopologyReal` `uniformContinuous_dist`
`dist_self` 📖	mathematical	—	`Dist.dist` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `instDist` `Real` `Real.instZero`	—	`induction_on` `isClosed_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace` `T3Space.toT0Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `instOrderTopologyReal` `UniformSpace.pseudoMetrizableSpace` `EMetric.instIsCountablyGeneratedUniformity` `continuous_dist` `continuous_id` `continuous_const` `dist_eq` `dist_self`
`dist_triangle` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `instDist` `Real.instAdd`	—	`induction_on₃` `isClosed_le` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `continuous_dist` `Continuous.fst` `continuous_id` `Continuous.snd` `Continuous.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `dist_eq` `dist_triangle`
`edist_eq` 📖	mathematical	—	`EDist.edist` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpace` `coe'` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`coe_isometry`
`instIsBoundedSMul` 📖	mathematical	—	`IsBoundedSMul` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `instZeroCompletion` `instSMul`	—	`induction_on₂` `isClosed_le` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Continuous.dist` `Continuous.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `instUniformContinuousConstSMul` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_const` `coe_smul` `IsBoundedSMul.toUniformContinuousConstSMul` `dist_eq` `dist_smul_pair` `induction_on` `coe_zero` `dist_pair_smul`
`mem_uniformity_dist` 📖	mathematical	—	`Set` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `Filter` `Filter.instMembership` `uniformity` `uniformSpace` `Real` `Real.instLT` `Real.instZero` `Set.instMembership`	—	`mem_uniformity_isClosed` `uniformContinuous_def` `uniformContinuous_coe` `Metric.mem_uniformity_dist` `induction_on₂` `Set.ext` `IsClosed.union` `isClosed_le` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `continuous_const` `UniformContinuous.continuous` `uniformContinuous_dist` `dist_eq` `not_le` `Metric.dist_mem_uniformity` `uniformity_prod_eq_prod` `Filter.mem_of_superset` `refl_mem_uniformity` `lt_of_le_of_lt` `le_abs_self` `dist_self` `dist_comm` `zero_sub` `abs_neg`
`uniformContinuous_dist` 📖	mathematical	—	`UniformContinuous` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `Real` `instUniformSpaceProd` `uniformSpace` `Real.pseudoMetricSpace` `Dist.dist` `instDist`	—	`uniformContinuous_extension₂` `Real.instCompleteSpace`
`uniformity_dist` 📖	mathematical	—	`uniformity` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `uniformSpace` `iInf` `Filter` `Real` `Filter.instInfSet` `Real.instLT` `Real.instZero` `Filter.principal` `setOf` `Dist.dist` `instDist`	—	`iInf_congr_Prop` `iInf_subtype` `uniformity_dist'`
`uniformity_dist'` 📖	mathematical	—	`uniformity` `UniformSpace.Completion` `PseudoMetricSpace.toUniformSpace` `uniformSpace` `iInf` `Filter` `Real` `Real.instLT` `Real.instZero` `Filter.instInfSet` `Filter.principal` `setOf` `Dist.dist` `instDist`	—	`Filter.ext` `Filter.mem_iInf_of_directed` `lt_min` `nonempty_gt` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`

---

← Back to Index