Completion

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

Statistics

Metric	Count
Definitions extensionHom, mapRingHom, instDist, instMetricSpace	4
Theorems completion_extension, completion_map, extensionHom_coe, isometry_mapRingHom, mapRingHom_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'	19
Total	23

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
mapRingHom 📖	CompOp	2 math math: isometry_mapRingHom, mapRingHom_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completion_extension 📖	mathematical	Isometry PseudoMetricSpace.toPseudoEMetricSpace	Isometry UniformSpace.Completion PseudoMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace PseudoMetricSpace.toPseudoEMetricSpace 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	Isometry 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	DFunLike.coe RingHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace Semiring.toNonAssocSemiring Ring.toSemiring UniformSpace.Completion.ring RingHom.instFunLike extensionHom UniformSpace.Completion.coe'	—	UniformSpace.Completion.extensionHom_coe continuous
isometry_mapRingHom 📖	mathematical	Isometry PseudoMetricSpace.toPseudoEMetricSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingHom.instFunLike	Isometry UniformSpace.Completion PseudoMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring UniformSpace.Completion.ring RingHom.instFunLike mapRingHom	—	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.comp₂ continuous_dist Continuous.comp UniformSpace.Completion.continuous_map continuous_fst continuous_snd Continuous.dist Continuous.fst continuous_id' Continuous.snd mapRingHom_coe UniformSpace.Completion.dist_eq dist_eq
mapRingHom_coe 📖	mathematical	Isometry PseudoMetricSpace.toPseudoEMetricSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingHom.instFunLike	DFunLike.coe RingHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace Semiring.toNonAssocSemiring Ring.toSemiring UniformSpace.Completion.ring RingHom.instFunLike mapRingHom UniformSpace.Completion.coe'	—	UniformSpace.Completion.mapRingHom_coe UniformContinuous.continuous uniformContinuous

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completion_extension 📖	mathematical	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace	LipschitzWith UniformSpace.Completion PseudoMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace 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.const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal UniformSpace.Completion.extension_coe MetricSpace.instT0Space uniformContinuous UniformSpace.Completion.dist_eq dist_le_mul
completion_map 📖	mathematical	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace	LipschitzWith 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	10 math math: uniformContinuous_dist, dist_eq, PadicComplex.isUltrametricDist, 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, Isometry.isometry_mapRingHom, 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	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist UniformSpace.Completion 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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.const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal coe_smul IsBoundedSMul.toUniformContinuousConstSMul dist_eq dist_smul_pair induction_on continuous_const 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