Completion

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

Statistics

Metric	Count
Definitions CauchyFilter, extend, gen, instInhabited, instUniformSpace, pureCauchy, Completion, inhabited, completeEquivSelf, cPkg, coe', completionSeparationQuotientEquiv, extension, extension₂, inhabited, instCoe, map, mapEquiv, map₂, uniformSpace	20
Theorems basis_uniformity, cauchyFilter_eq, denseRange_pureCauchy, extend_pureCauchy, inseparable_iff, inseparable_iff_of_le_nhds, inseparable_lim_iff, instCompleteSpace, instNeBotValFilterCauchy, instNonempty, isDenseEmbedding_pureCauchy, isDenseInducing_pureCauchy, isUniformEmbedding_pureCauchy, isUniformInducing_pureCauchy, mem_uniformity, mem_uniformity', monotone_gen, nonempty_cauchyFilter_iff, separated_pureCauchy_injective, uniformContinuous_extend, coe_eq, coe_inj, coe_injective, comap_coe_eq_uniformity, completeSpace, continuous_coe, continuous_extension, continuous_map, continuous_map₂, denseRange_coe, denseRange_coe₂, denseRange_coe₃, ext, ext', extension_coe, extension_comp_coe, extension_map, extension_unique, extension₂_coe_coe, induction_on, induction_on₂, induction_on₃, inseparable_extension_coe, isDenseEmbedding_coe, isDenseInducing_coe, isUniformEmbedding_coe, isUniformInducing_coe, isUniformInducing_extension, mapEquiv_coe, mapEquiv_symm, map_coe, map_comp, map_id, map_unique, map₂_coe_coe, nonempty_completion_iff, separableSpace_completion, t0Space, uniformContinuous_coe, uniformContinuous_completionSeparationQuotientEquiv, uniformContinuous_completionSeparationQuotientEquiv_symm, uniformContinuous_extension, uniformContinuous_extension₂, uniformContinuous_map, uniformContinuous_map₂	65
Total	85

CauchyFilter

Definitions

Name	Category	Theorems
extend 📖	CompOp	2 math math: extend_pureCauchy, uniformContinuous_extend
gen 📖	CompOp	7 math math: isTrans_gen, IsSymmetricRel.cauchyFilter_gen, mem_uniformity, isSymm_gen, basis_uniformity, monotone_gen, IsTransitiveRel.cauchyFilter_gen
instInhabited 📖	CompOp	—
instUniformSpace 📖	CompOp	18 math math: isUniformInducing_pureCauchy, mem_uniformity', mem_uniformity, cauchyFilter_eq, inseparable_iff, denseRange_pureCauchy, basis_uniformity, separated_pureCauchy_injective, UniformSpace.Completion.coe_eq, isDenseEmbedding_pureCauchy, isUniformEmbedding_pureCauchy, instCompleteSpace, IsUltraUniformity.cauchyFilter, uniformContinuous_extend, inseparable_iff_of_le_nhds, IsUltraUniformity.cauchyFilter_iff, isDenseInducing_pureCauchy, inseparable_lim_iff
pureCauchy 📖	CompOp	8 math math: isUniformInducing_pureCauchy, denseRange_pureCauchy, separated_pureCauchy_injective, UniformSpace.Completion.coe_eq, isDenseEmbedding_pureCauchy, isUniformEmbedding_pureCauchy, extend_pureCauchy, isDenseInducing_pureCauchy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_uniformity 📖	mathematical	Filter.HasBasis uniformity	CauchyFilter instUniformSpace SetRel Set gen	—	Filter.HasBasis.lift' monotone_gen
cauchyFilter_eq 📖	mathematical	—	lim UniformSpace.toTopologicalSpace Filter.NeBot.nonempty Filter Cauchy Filter.NeBot Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SProd.sprod Filter.instSProd uniformity Inseparable CauchyFilter instUniformSpace	—	Filter.NeBot.nonempty inseparable_iff_eq inseparable_lim_iff
denseRange_pureCauchy 📖	mathematical	—	DenseRange CauchyFilter UniformSpace.toTopologicalSpace instUniformSpace pureCauchy	—	Filter.mem_lift'_sets monotone_gen comp_mem_uniformity_sets Filter.mem_prod_same_iff Filter.NeBot.nonempty_of_mem Filter.mem_prod_iff Set.mk_mem_prod SetRel.prodMk_mem_comp closure_eq_cluster_pts nhds_eq_uniformity Filter.lift'_inf_principal_eq Set.inter_comm Filter.lift'_neBot_iff Monotone.inter monotone_const Set.monotone_preimage Set.mem_range_self
extend_pureCauchy 📖	mathematical	UniformContinuous	extend pureCauchy	—	isDenseInducing_pureCauchy extend.eq_1 uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy
inseparable_iff 📖	mathematical	—	Inseparable CauchyFilter UniformSpace.toTopologicalSpace instUniformSpace Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SProd.sprod Filter.instSProd Cauchy uniformity	—	Filter.HasBasis.inseparable_iff_uniformity basis_uniformity Filter.basis_sets
inseparable_iff_of_le_nhds 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Cauchy nhds UniformSpace.toTopologicalSpace	Inseparable CauchyFilter instUniformSpace	—	inseparable_iff Filter.Tendsto.inseparable_iff_uniformity Filter.prod.instNeBot instNeBotValFilterCauchy Filter.Tendsto.comp Filter.tendsto_id' Filter.tendsto_fst Filter.tendsto_snd
inseparable_lim_iff 📖	mathematical	—	Inseparable UniformSpace.toTopologicalSpace lim Filter.NeBot.nonempty Filter Cauchy Filter.NeBot Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SProd.sprod Filter.instSProd uniformity CauchyFilter instUniformSpace	—	inseparable_iff_of_le_nhds Filter.NeBot.nonempty Cauchy.le_nhds_lim
instCompleteSpace 📖	mathematical	—	CompleteSpace CauchyFilter instUniformSpace	—	completeSpace_extension isUniformInducing_pureCauchy denseRange_pureCauchy Filter.le_lift' Filter.mem_lift'_sets monotone_gen Filter.mem_prod_same_iff Filter.sets_of_superset Filter.prod_mem_prod Set.Subset.trans Set.preimage_mono nhds_eq_uniformity
instNeBotValFilterCauchy 📖	mathematical	—	Filter.NeBot Filter Cauchy	—	—
instNonempty 📖	mathematical	—	CauchyFilter	—	—
isDenseEmbedding_pureCauchy 📖	mathematical	—	IsDenseEmbedding CauchyFilter UniformSpace.toTopologicalSpace instUniformSpace pureCauchy	—	IsUniformEmbedding.isDenseEmbedding isUniformEmbedding_pureCauchy denseRange_pureCauchy
isDenseInducing_pureCauchy 📖	mathematical	—	IsDenseInducing CauchyFilter UniformSpace.toTopologicalSpace instUniformSpace pureCauchy	—	IsUniformInducing.isDenseInducing isUniformInducing_pureCauchy denseRange_pureCauchy
isUniformEmbedding_pureCauchy 📖	mathematical	—	IsUniformEmbedding CauchyFilter instUniformSpace pureCauchy	—	isUniformInducing_pureCauchy Filter.pure_injective
isUniformInducing_pureCauchy 📖	mathematical	—	IsUniformInducing CauchyFilter instUniformSpace pureCauchy	—	Set.ext cauchy_pure Filter.prod_pure Filter.comap_lift'_eq Filter.lift'_id
mem_uniformity 📖	mathematical	—	Set CauchyFilter Filter Filter.instMembership uniformity instUniformSpace SetRel Set.instHasSubset gen	—	Filter.mem_lift'_sets monotone_gen
mem_uniformity' 📖	mathematical	—	Set CauchyFilter Filter Filter.instMembership uniformity instUniformSpace Set.instMembership	—	mem_uniformity
monotone_gen 📖	mathematical	—	Monotone SetRel CauchyFilter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra gen	—	Set.monotone_setOf Filter.monotone_mem
nonempty_cauchyFilter_iff 📖	mathematical	—	CauchyFilter	—	Set.eq_univ_iff_forall IsDenseInducing.closure_range IsDenseEmbedding.isDenseInducing isDenseEmbedding_pureCauchy mem_closure_iff isOpen_univ
separated_pureCauchy_injective 📖	mathematical	—	SeparationQuotient CauchyFilter UniformSpace.toTopologicalSpace instUniformSpace pureCauchy	—	Inseparable.eq inseparable_iff_of_le_nhds pure_le_nhds
uniformContinuous_extend 📖	mathematical	—	UniformContinuous CauchyFilter instUniformSpace extend	—	isDenseInducing_pureCauchy extend.eq_1 uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy uniformContinuous_of_const

UniformSpace

Definitions

Name	Category	Theorems
Completion 📖	CompOp	167 math math: Valued.continuous_extension, Asymptotics.isTheta_completion_right, NormedAddGroupHom.completion_def, AddMonoidHom.completion_coe, Completion.mul_hatInv_cancel, Asymptotics.isLittleO_completion_left, Completion.vadd_def, Completion.mapRingHom_id, Asymptotics.isLittleO_completion_right, Completion.instNontrivialOfT0Space, Valued.valuedCompletion_surjective_iff, Isometry.extensionHom_coe, PadicComplex.valuation_extends, LipschitzWith.completion_extension, Completion.uniformContinuous_extension₂, NormedAddCommGroup.norm_toCompl, Completion.mem_uniformity_dist, NormedAddGroupHom.zero_completion, Valuation.IsEquiv.valuedCompletion_le_one_iff, Completion.smul_def, NumberField.InfinitePlace.Completion.norm_coe, Completion.extensionHom_coe, Completion.coe_eq_one_iff, Completion.uniformContinuous_dist, NormedAddGroupHom.extension_coe_to_fun, Valued.exists_coe_eq_v, Completion.instSMulCommClassOfUniformContinuousConstSMul, NormedAddGroupHom.norm_completion, Completion.map_smul_eq_mul_coe, Completion.mapRingHom_apply, Completion.nnnorm_coe, Valued.extension_eq_zero_iff, Completion.continuous_hatInv, NormedAddGroupHom.completion_sub, Completion.mapEquiv_coe, Isometry.completion_map, NormedAddGroupHom.completion_coe, Completion.isUniformInducing_extension, Completion.instUniformContinuousConstSMul, NormedAddCommGroup.denseRange_toCompl, Completion.dist_eq, Completion.coe_vadd, Completion.instContinuousMul, Completion.separableSpace_completion, Completion.instUniformContinuousConstVAdd, Completion.extension_map, NormedAddGroupHom.extension_coe, Completion.norm_toComplL, Completion.denseRange_coe, AddMonoidHom.extension_coe, Valued.continuous_extensionValuation, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', NormedAddGroupHom.completion_add, Asymptotics.isBigO_completion_right, normedAddGroupHomCompletionHom_apply, UniformSpaceCat.completionFunctor_map, Completion.map_comp, Completion.isUniformEmbedding_coe, Completion.continuous_coeRingHom, Completion.coe_isometry, Completion.uniformContinuous_extension, AddMonoidHom.continuous_completion, Isometry.completion_extension, NormedAddGroupHom.completion_coe_to_fun, AddMonoidHom.completion_add, Valued.closure_coe_completion_v_lt, Completion.algebraMap_def, Completion.completeSpace, Completion.norm_coe, Valued.closure_coe_completion_v_mul_v_lt, Valued.valuedCompletion_apply, IsUltraUniformity.completion, Completion.denseRange_coe₃, Completion.coe_neg, Summable.toCompl_tsum, Completion.continuous_coe, Completion.instVAddAssocClass, Completion.coe_eq_zero_iff, Completion.instIsTopologicalDivisionRing, Completion.coe_toComplₗᵢ, Completion.coe_zero, LipschitzWith.completion_map, Completion.coe_smul, NormedAddGroupHom.ker_completion, SemiNormedGrp.completion_obj_str, Completion.isUniformAddGroup, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, ContinuousLinearMap.completion_apply_coe, Completion.uniformContinuous_completionSeparationQuotientEquiv_symm, Completion.instIsCentralVAdd, PadicComplex.coe_zero, Completion.nonempty_completion_iff, Completion.uniformity_dist, NormedAddGroupHom.completion_toCompl, NormedAddGroupHom.completion_neg, AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp, Completion.t0Space, Completion.continuous_map, Completion.continuous_extension, Valued.extensionValuation_apply_coe, Completion.mapRingHom_coe, Completion.coe_mul, Completion.mapRingEquiv_apply, Completion.uniformContinuous_coe, ContinuousLinearMap.toAddMonoidHom_completion, Completion.dist_comm, Asymptotics.isTheta_completion_left, NormedAddCommGroup.toCompl_apply, AddMonoidHom.continuous_extension, Completion.uniformContinuous_map₂, instNonarchimedeanAddGroupCompletion, PadicComplex.norm_extends, Completion.coe_mapRingHom, Completion.mapEquiv_symm, summable_iff_cauchySeq_finset_and_tsum_mem, Completion.enorm_coe, NormedAddGroupHom.ker_le_ker_completion, IsUltraUniformity.completion_iff, Completion.coe_toComplL, Padic.coe_withValRingEquiv_symm, NormedAddGroupHom.completion_comp, LaurentSeries.comparePkg_eq_extension, Completion.denseRange_coe₂, NormedAddGroupHom.extension_def, Completion.continuous_toCompl, instNonarchimedeanRingCompletion, Valued.instFaithfulSMulCompletionOfUniformContinuousConstSMul, Completion.inner_coe, Completion.mapRingHom_comp, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, Completion.instIsCentralScalar, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, Completion.dist_triangle, Completion.coe_injective, Completion.coe_sub, Completion.uniformContinuous_completionSeparationQuotientEquiv, Completion.comap_coe_eq_uniformity, summable_iff_summable_compl_and_tsum_mem, Completion.continuous_inner, Completion.map_id, Completion.isDenseInducing_toCompl, Completion.instIsBoundedSMul, Completion.mapRingEquiv_symm_apply, Asymptotics.isBigO_completion_left, Completion.toCompl_apply, AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp, AddMonoidHom.completion_zero, PadicComplex.nnnorm_extends, Completion.instVAddCommClassOfUniformContinuousConstVAdd, Completion.edist_eq, SemiNormedGrp.completion_map, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe, SemiNormedGrp.completion_obj_carrier, NormedAddGroupHom.completion_id, Completion.uniformity_dist', Completion.isDenseInducing_coe, Completion.coe_add, Completion.dist_self, Completion.coe_one, Completion.instIsScalarTower, Completion.isDenseEmbedding_coe, Completion.topologicalRing, Completion.uniformContinuous_map, hasSum_iff_hasSum_compl, Completion.isUniformInducing_coe, ContinuousLinearMap.coe_completion, Completion.coe_inv

UniformSpace.Completion

Definitions

Name	Category	Theorems
cPkg 📖	CompOp	—
coe' 📖	CompOp	95 math math: Asymptotics.isTheta_completion_right, AddMonoidHom.completion_coe, UniformSpaceCat.completionHom_val, Asymptotics.isLittleO_completion_left, Asymptotics.isLittleO_completion_right, Valued.extension_extends, Isometry.extensionHom_coe, PadicComplex.valuation_extends, PadicComplex.coe_eq, NumberField.FinitePlace.embedding_apply, NumberField.InfiniteAdeleRing.algebraMap_apply, NumberField.InfinitePlace.Completion.norm_coe, PadicComplex.coe_natCast, extensionHom_coe, coe_eq_one_iff, map_smul_eq_mul_coe, nnnorm_coe, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, extension_coe, extension₂_coe_coe, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, mapEquiv_coe, NormedAddGroupHom.completion_coe, dist_eq, coe_vadd, map_coe, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe, NormedAddGroupHom.extension_coe, denseRange_coe, AddMonoidHom.extension_coe, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', Asymptotics.isBigO_completion_right, coe_inj, isUniformEmbedding_coe, coe_isometry, LaurentSeries.coe_X_compare, Valued.closure_coe_completion_v_lt, algebraMap_def, norm_coe, Valued.closure_coe_completion_v_mul_v_lt, Valued.valuedCompletion_apply, coe_eq, denseRange_coe₃, coe_neg, Summable.toCompl_tsum, continuous_coe, coe_eq_zero_iff, coe_toComplₗᵢ, NumberField.InfinitePlace.Completion.extensionEmbedding_coe, coe_zero, map₂_coe_coe, coe_smul, ContinuousLinearMap.completion_apply_coe, PadicComplex.coe_zero, extension_comp_coe, Valued.extensionValuation_apply_coe, mapRingHom_coe, Padic.withValUniformEquiv_cast_apply, coe_mul, NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal_coe, uniformContinuous_coe, Asymptotics.isTheta_completion_left, NormedAddCommGroup.toCompl_apply, LaurentSeries.tendsto_valuation, PadicComplex.norm_extends, NumberField.AdeleRing.algebraMap_fst_apply, enorm_coe, coe_toComplL, Padic.coe_withValRingEquiv_symm, denseRange_coe₂, NormedAddGroupHom.extension_def, inner_coe, NormedAddGroupHom.completion_coe', IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, coe_injective, coe_sub, comap_coe_eq_uniformity, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, Asymptotics.isBigO_completion_left, toCompl_apply, PadicComplex.nnnorm_extends, edist_eq, hatInv_extends, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe, isDenseInducing_coe, coe_add, coe_one, isDenseEmbedding_coe, hasSum_iff_hasSum_compl, isUniformInducing_coe, coe_inv, inseparable_extension_coe
completionSeparationQuotientEquiv 📖	CompOp	2 math math: uniformContinuous_completionSeparationQuotientEquiv_symm, uniformContinuous_completionSeparationQuotientEquiv
extension 📖	CompOp	14 math math: LipschitzWith.completion_extension, NormedAddGroupHom.extension_coe_to_fun, extension_coe, isUniformInducing_extension, extension_map, uniformContinuous_extension, Isometry.completion_extension, extension_comp_coe, continuous_extension, Padic.coe_withValRingEquiv, NormedAddGroupHom.extension_def, UniformSpaceCat.extensionHom_val, extension_unique, inseparable_extension_coe
extension₂ 📖	CompOp	2 math math: uniformContinuous_extension₂, extension₂_coe_coe
inhabited 📖	CompOp	—
instCoe 📖	CompOp	—
map 📖	CompOp	21 math math: NormedAddGroupHom.completion_def, vadd_def, smul_def, map_smul_eq_mul_coe, mapRingHom_apply, Isometry.completion_map, map_coe, extension_map, UniformSpaceCat.completionFunctor_map, map_comp, NormedAddGroupHom.completion_coe_to_fun, LipschitzWith.completion_map, continuous_map, mapRingEquiv_apply, coe_mapRingHom, NormedAddGroupHom.completion_coe', map_unique, map_id, mapRingEquiv_symm_apply, uniformContinuous_map, ContinuousLinearMap.coe_completion
mapEquiv 📖	CompOp	3 math math: Valuation.IsEquiv.valuedCompletion_le_one_iff, mapEquiv_coe, mapEquiv_symm
map₂ 📖	CompOp	3 math math: continuous_map₂, map₂_coe_coe, uniformContinuous_map₂
uniformSpace 📖	CompOp	77 math math: Valued.continuous_extension, Padic.withValUniformEquiv_norm_le_one_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, uniformContinuous_extension₂, mem_uniformity_dist, Valuation.IsEquiv.valuedCompletion_le_one_iff, uniformContinuous_dist, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, continuous_hatInv, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, AbsoluteValue.Completion.locallyCompactSpace, mapEquiv_coe, isUniformInducing_extension, instUniformContinuousConstSMul, NumberField.InfinitePlace.Completion.locallyCompactSpace, NormedAddCommGroup.denseRange_toCompl, instContinuousMul, separableSpace_completion, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, instUniformContinuousConstVAdd, norm_toComplL, denseRange_coe, Valued.continuous_extensionValuation, UniformSpaceCat.completionFunctor_map, isUniformEmbedding_coe, continuous_coeRingHom, PadicInt.coe_adicCompletionIntegersEquiv_apply, uniformContinuous_extension, AddMonoidHom.continuous_completion, Valued.closure_coe_completion_v_lt, completeSpace, Valued.closure_coe_completion_v_mul_v_lt, PositiveLinearMap.gnsStarAlgHom_apply, IsUltraUniformity.completion, denseRange_coe₃, Summable.toCompl_tsum, continuous_coe, instIsTopologicalDivisionRing, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, NormedAddGroupHom.ker_completion, isUniformAddGroup, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, ContinuousLinearMap.completion_apply_coe, uniformContinuous_completionSeparationQuotientEquiv_symm, uniformity_dist, t0Space, continuous_map, continuous_extension, Padic.withValUniformEquiv_cast_apply, uniformContinuous_coe, ContinuousLinearMap.toAddMonoidHom_completion, AddMonoidHom.continuous_extension, uniformContinuous_map₂, instNonarchimedeanAddGroupCompletion, mapEquiv_symm, summable_iff_cauchySeq_finset_and_tsum_mem, IsUltraUniformity.completion_iff, coe_toComplL, Padic.coe_withValRingEquiv_symm, denseRange_coe₂, continuous_toCompl, instNonarchimedeanRingCompletion, uniformContinuous_completionSeparationQuotientEquiv, comap_coe_eq_uniformity, summable_iff_summable_compl_and_tsum_mem, continuous_inner, isDenseInducing_toCompl, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, uniformity_dist', isDenseInducing_coe, isDenseEmbedding_coe, topologicalRing, uniformContinuous_map, hasSum_iff_hasSum_compl, isUniformInducing_coe, ContinuousLinearMap.coe_completion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq 📖	mathematical	—	coe' CauchyFilter SeparationQuotient UniformSpace.toTopologicalSpace CauchyFilter.instUniformSpace CauchyFilter.pureCauchy	—	—
coe_inj 📖	mathematical	—	coe'	—	coe_injective
coe_injective 📖	mathematical	—	UniformSpace.Completion coe'	—	IsUniformEmbedding.injective isUniformEmbedding_coe
comap_coe_eq_uniformity 📖	mathematical	—	Filter.comap UniformSpace.Completion coe' uniformity uniformSpace	—	IsUniformInducing.comap_uniformity isUniformInducing_coe
completeSpace 📖	mathematical	—	CompleteSpace UniformSpace.Completion uniformSpace	—	SeparationQuotient.instCompleteSpace CauchyFilter.instCompleteSpace
continuous_coe 📖	mathematical	—	Continuous UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace coe'	—	AbstractCompletion.continuous_coe
continuous_extension 📖	mathematical	—	Continuous UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace extension	—	AbstractCompletion.continuous_extend
continuous_map 📖	mathematical	—	Continuous UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace map	—	AbstractCompletion.continuous_map
continuous_map₂ 📖	mathematical	Continuous UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace	map₂	—	AbstractCompletion.continuous_map₂
denseRange_coe 📖	mathematical	—	DenseRange UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace coe'	—	DenseRange.comp Function.Surjective.denseRange CauchyFilter.denseRange_pureCauchy
denseRange_coe₂ 📖	mathematical	—	DenseRange UniformSpace.Completion instTopologicalSpaceProd UniformSpace.toTopologicalSpace uniformSpace coe'	—	DenseRange.prodMap denseRange_coe
denseRange_coe₃ 📖	mathematical	—	DenseRange UniformSpace.Completion instTopologicalSpaceProd UniformSpace.toTopologicalSpace uniformSpace coe'	—	DenseRange.prodMap denseRange_coe denseRange_coe₂
ext 📖	—	Continuous UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace coe'	—	—	AbstractCompletion.funext
ext' 📖	—	Continuous UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace coe'	—	—	ext
extension_coe 📖	mathematical	UniformContinuous	extension coe'	—	AbstractCompletion.extend_coe T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace
extension_comp_coe 📖	mathematical	UniformContinuous UniformSpace.Completion uniformSpace	extension coe'	—	AbstractCompletion.extend_comp_coe
extension_map 📖	mathematical	UniformContinuous	UniformSpace.Completion extension map	—	ext T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace Continuous.comp continuous_extension continuous_map map_coe extension_coe UniformContinuous.comp
extension_unique 📖	mathematical	UniformContinuous UniformSpace.Completion uniformSpace coe'	extension	—	AbstractCompletion.extend_unique
extension₂_coe_coe 📖	mathematical	UniformContinuous₂	extension₂ coe'	—	AbstractCompletion.extension₂_coe_coe
induction_on 📖	—	coe'	—	—	isClosed_property denseRange_coe
induction_on₂ 📖	—	coe'	—	—	isClosed_property denseRange_coe₂
induction_on₃ 📖	—	coe'	—	—	isClosed_property denseRange_coe₃
inseparable_extension_coe 📖	mathematical	UniformContinuous	Inseparable UniformSpace.toTopologicalSpace extension coe'	—	AbstractCompletion.inseparable_extend_coe
isDenseEmbedding_coe 📖	mathematical	—	IsDenseEmbedding UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace coe'	—	isDenseInducing_coe CauchyFilter.separated_pureCauchy_injective
isDenseInducing_coe 📖	mathematical	—	IsDenseInducing UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace coe'	—	IsUniformInducing.isInducing isUniformInducing_coe denseRange_coe
isUniformEmbedding_coe 📖	mathematical	—	IsUniformEmbedding UniformSpace.Completion uniformSpace coe'	—	comap_coe_eq_uniformity CauchyFilter.separated_pureCauchy_injective
isUniformInducing_coe 📖	mathematical	—	IsUniformInducing UniformSpace.Completion uniformSpace coe'	—	IsUniformInducing.comp CauchyFilter.isUniformInducing_pureCauchy
isUniformInducing_extension 📖	mathematical	IsUniformInducing	UniformSpace.Completion uniformSpace extension	—	AbstractCompletion.isUniformInducing_extend
mapEquiv_coe 📖	mathematical	—	DFunLike.coe UniformEquiv UniformSpace.Completion uniformSpace EquivLike.toFunLike UniformEquiv.instEquivLike mapEquiv coe'	—	AbstractCompletion.mapEquiv_coe
mapEquiv_symm 📖	mathematical	—	UniformEquiv.symm UniformSpace.Completion uniformSpace mapEquiv	—	AbstractCompletion.mapEquiv_symm
map_coe 📖	mathematical	UniformContinuous	map coe'	—	AbstractCompletion.map_coe
map_comp 📖	mathematical	UniformContinuous	UniformSpace.Completion map	—	extension_map completeSpace t0Space UniformContinuous.comp uniformContinuous_coe
map_id 📖	mathematical	—	map UniformSpace.Completion	—	AbstractCompletion.map_id
map_unique 📖	mathematical	UniformContinuous UniformSpace.Completion uniformSpace coe'	map	—	AbstractCompletion.map_unique
map₂_coe_coe 📖	mathematical	UniformContinuous₂	map₂ coe'	—	AbstractCompletion.map₂_coe_coe
nonempty_completion_iff 📖	mathematical	—	UniformSpace.Completion	—	DenseRange.nonempty_iff AbstractCompletion.dense
separableSpace_completion 📖	mathematical	—	TopologicalSpace.SeparableSpace UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace	—	IsDenseInducing.separableSpace isDenseInducing_coe
t0Space 📖	mathematical	—	T0Space UniformSpace.Completion UniformSpace.toTopologicalSpace uniformSpace	—	SeparationQuotient.instT0Space
uniformContinuous_coe 📖	mathematical	—	UniformContinuous UniformSpace.Completion uniformSpace coe'	—	AbstractCompletion.uniformContinuous_coe
uniformContinuous_completionSeparationQuotientEquiv 📖	mathematical	—	UniformContinuous UniformSpace.Completion SeparationQuotient UniformSpace.toTopologicalSpace SeparationQuotient.instUniformSpace uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike completionSeparationQuotientEquiv	—	uniformContinuous_extension t0Space completeSpace
uniformContinuous_completionSeparationQuotientEquiv_symm 📖	mathematical	—	UniformContinuous UniformSpace.Completion SeparationQuotient UniformSpace.toTopologicalSpace SeparationQuotient.instUniformSpace uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm completionSeparationQuotientEquiv	—	uniformContinuous_map
uniformContinuous_extension 📖	mathematical	—	UniformContinuous UniformSpace.Completion uniformSpace extension	—	AbstractCompletion.uniformContinuous_extend
uniformContinuous_extension₂ 📖	mathematical	—	UniformContinuous₂ UniformSpace.Completion uniformSpace extension₂	—	AbstractCompletion.uniformContinuous_extension₂
uniformContinuous_map 📖	mathematical	—	UniformContinuous UniformSpace.Completion uniformSpace map	—	AbstractCompletion.uniformContinuous_map
uniformContinuous_map₂ 📖	mathematical	—	UniformContinuous₂ UniformSpace.Completion uniformSpace map₂	—	AbstractCompletion.uniformContinuous_map₂

UniformSpace.Completion.AbstractCompletion

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

UniformSpace.Completion.UniformCompletion

Definitions

Name	Category	Theorems
completeEquivSelf 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
CauchyFilter 📖	CompOp	25 math math: CauchyFilter.isTrans_gen, CauchyFilter.isUniformInducing_pureCauchy, CauchyFilter.mem_uniformity', IsSymmetricRel.cauchyFilter_gen, CauchyFilter.mem_uniformity, CauchyFilter.cauchyFilter_eq, CauchyFilter.inseparable_iff, CauchyFilter.isSymm_gen, CauchyFilter.denseRange_pureCauchy, CauchyFilter.basis_uniformity, CauchyFilter.monotone_gen, CauchyFilter.separated_pureCauchy_injective, UniformSpace.Completion.coe_eq, CauchyFilter.isDenseEmbedding_pureCauchy, CauchyFilter.isUniformEmbedding_pureCauchy, CauchyFilter.instCompleteSpace, IsUltraUniformity.cauchyFilter, IsTransitiveRel.cauchyFilter_gen, CauchyFilter.uniformContinuous_extend, CauchyFilter.inseparable_iff_of_le_nhds, IsUltraUniformity.cauchyFilter_iff, CauchyFilter.isDenseInducing_pureCauchy, CauchyFilter.inseparable_lim_iff, CauchyFilter.nonempty_cauchyFilter_iff, CauchyFilter.instNonempty

---

← Back to Index