Completion

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

Statistics

Metric	Count
Definitions Completion, Completion	2
Theorems isSymm_gen, isTrans_gen, cauchyFilter_gen, cauchyFilter_gen, cauchyFilter, cauchyFilter_iff, completion, completion_iff, separationQuotient, separationQuotient_iff, isUltraUniformity	11
Total	13

AbsoluteValue

Definitions

Name	Category	Theorems
Completion 📖	CompOp	2 math math: Completion.locallyCompactSpace, Completion.extensionEmbedding_dist_eq_of_comp

CauchyFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymm_gen 📖	mathematical	—	SetRel.IsSymm CauchyFilter gen	—	SetRel.mem_filter_prod_comm
isTrans_gen 📖	mathematical	—	SetRel.IsTrans CauchyFilter gen	—	IsTransitiveRel.mem_filter_prod_trans instNeBotValFilterCauchy

IsSymmetricRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchyFilter_gen 📖	mathematical	—	SetRel.IsSymm CauchyFilter CauchyFilter.gen	—	CauchyFilter.isSymm_gen

IsTransitiveRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchyFilter_gen 📖	mathematical	—	SetRel.IsTrans CauchyFilter CauchyFilter.gen	—	CauchyFilter.isTrans_gen

IsUltraUniformity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchyFilter 📖	mathematical	—	IsUltraUniformity CauchyFilter CauchyFilter.instUniformSpace	—	mk_of_hasBasis CauchyFilter.basis_uniformity hasBasis CauchyFilter.isSymm_gen CauchyFilter.isTrans_gen
cauchyFilter_iff 📖	mathematical	—	IsUltraUniformity CauchyFilter CauchyFilter.instUniformSpace	—	IsUniformInducing.isUltraUniformity CauchyFilter.isUniformInducing_pureCauchy cauchyFilter
completion 📖	mathematical	—	IsUltraUniformity UniformSpace.Completion UniformSpace.Completion.uniformSpace	—	completion_iff
completion_iff 📖	mathematical	—	IsUltraUniformity UniformSpace.Completion UniformSpace.Completion.uniformSpace	—	cauchyFilter_iff separationQuotient_iff
separationQuotient 📖	mathematical	—	IsUltraUniformity SeparationQuotient UniformSpace.toTopologicalSpace SeparationQuotient.instUniformSpace	—	Filter.HasBasis.map hasBasis mk_of_hasBasis SeparationQuotient.uniformity_eq SetRel.isSymm_image Filter.mem_ker inseparable_iff_ker_uniformity SetRel.trans
separationQuotient_iff 📖	mathematical	—	IsUltraUniformity SeparationQuotient UniformSpace.toTopologicalSpace SeparationQuotient.instUniformSpace	—	IsUniformInducing.isUltraUniformity separationQuotient

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUltraUniformity 📖	mathematical	IsUniformInducing	IsUltraUniformity	—	IsUltraUniformity.comap comap_uniformSpace

Valuation

Definitions

Name	Category	Theorems
Completion 📖	CompOp	6 math math: Padic.withValUniformEquiv_norm_le_one_iff, IsEquiv.valuedCompletion_le_one_iff, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, Padic.coe_withValRingEquiv_symm

---

← Back to Index