Completion

📁 Source: Mathlib/Analysis/Normed/Group/Completion.lean

Statistics

Metric	Count
Definitions instNorm, instNormedAddCommGroup	2
Theorems enorm_coe, nnnorm_coe, norm_coe	3
Total	5

UniformSpace.Completion

Definitions

Name	Category	Theorems
instNorm 📖	CompOp	10 math math: Asymptotics.isTheta_completion_right, Asymptotics.isLittleO_completion_left, Asymptotics.isLittleO_completion_right, NormedAddCommGroup.norm_toCompl, NumberField.InfinitePlace.Completion.norm_coe, Asymptotics.isBigO_completion_right, norm_coe, Asymptotics.isTheta_completion_left, Asymptotics.isBigO_completion_left, NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion
instNormedAddCommGroup 📖	CompOp	30 math math: NormedAddGroupHom.completion_def, NormedAddCommGroup.norm_toCompl, NormedAddGroupHom.zero_completion, NormedAddGroupHom.extension_coe_to_fun, NormedAddGroupHom.norm_completion, nnnorm_coe, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, NormedAddGroupHom.completion_sub, NormedAddGroupHom.completion_coe, NormedAddCommGroup.denseRange_toCompl, NormedAddGroupHom.extension_coe, norm_toComplL, NormedAddGroupHom.completion_add, normedAddGroupHomCompletionHom_apply, NormedAddGroupHom.completion_coe_to_fun, PositiveLinearMap.gnsStarAlgHom_apply, coe_toComplₗᵢ, NormedAddGroupHom.ker_completion, SemiNormedGrp.completion_obj_str, NormedAddGroupHom.completion_toCompl, NormedAddGroupHom.completion_neg, NormedAddCommGroup.toCompl_apply, enorm_coe, NormedAddGroupHom.ker_le_ker_completion, coe_toComplL, NormedAddGroupHom.completion_comp, NormedAddGroupHom.extension_def, SemiNormedGrp.completion_map, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, NormedAddGroupHom.completion_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_coe 📖	mathematical	—	ENorm.enorm UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup SeminormedAddGroup.toContinuousENorm coe'	—	nnnorm_coe
nnnorm_coe 📖	mathematical	—	NNNorm.nnnorm UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup coe'	—	norm_nonneg norm_coe
norm_coe 📖	mathematical	—	Norm.norm UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm SeminormedAddCommGroup.toNorm coe'	—	extension_coe T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal uniformContinuous_norm

---

← Back to Index