Completion

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

Statistics

Metric	Count
Definitions completion, incl, mapHom, instPreadditive	4
Theorems lift_comp_incl, lift_unique, map_normNoninc, map_zero, norm_incl_eq, completion_completeSpace, completion_map, completion_obj_carrier, completion_obj_str, instAdditiveCompletion	10
Total	14

SemiNormedGrp

Definitions

Name	Category	Theorems
completion 📖	CompOp	9 math math: completion.norm_incl_eq, instAdditiveCompletion, completion.map_normNoninc, completion_obj_str, completion.lift_comp_incl, completion.map_zero, completion_map, completion_obj_carrier, completion_completeSpace
instPreadditive 📖	CompOp	1 math math: instAdditiveCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completion_completeSpace 📖	mathematical	—	CompleteSpace carrier CategoryTheory.Functor.obj SemiNormedGrp instLargeCategory completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace str	—	UniformSpace.Completion.completeSpace
completion_map 📖	mathematical	—	CategoryTheory.Functor.map SemiNormedGrp instLargeCategory completion ofHom UniformSpace.Completion carrier PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace str NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup NormedAddGroupHom.completion Hom.hom	—	—
completion_obj_carrier 📖	mathematical	—	carrier CategoryTheory.Functor.obj SemiNormedGrp instLargeCategory completion UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace str	—	—
completion_obj_str 📖	mathematical	—	str CategoryTheory.Functor.obj SemiNormedGrp instLargeCategory completion NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion carrier PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNormedAddCommGroup	—	—
instAdditiveCompletion 📖	mathematical	—	CategoryTheory.Functor.Additive SemiNormedGrp instLargeCategory instPreadditive completion	—	hom_ext NormedAddGroupHom.completion_add

SemiNormedGrp.completion

Definitions

Name	Category	Theorems
incl 📖	CompOp	2 math math: norm_incl_eq, lift_comp_incl
mapHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_comp_incl 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SemiNormedGrp CategoryTheory.Category.toCategoryStruct SemiNormedGrp.instLargeCategory CategoryTheory.Functor.obj SemiNormedGrp.completion incl lift	—	SemiNormedGrp.ext NormedAddGroupHom.extension_coe
lift_unique 📖	mathematical	CategoryTheory.CategoryStruct.comp SemiNormedGrp CategoryTheory.Category.toCategoryStruct SemiNormedGrp.instLargeCategory CategoryTheory.Functor.obj SemiNormedGrp.completion incl	lift	—	SemiNormedGrp.hom_ext NormedAddGroupHom.extension_unique SemiNormedGrp.ext_iff
map_normNoninc 📖	mathematical	NormedAddGroupHom.NormNoninc SemiNormedGrp.carrier SemiNormedGrp.str SemiNormedGrp.Hom.hom	CategoryTheory.Functor.obj SemiNormedGrp SemiNormedGrp.instLargeCategory SemiNormedGrp.completion CategoryTheory.Functor.map	—	NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one LE.le.trans Eq.le NormedAddGroupHom.norm_completion
map_zero 📖	mathematical	—	CategoryTheory.Functor.map SemiNormedGrp SemiNormedGrp.instLargeCategory SemiNormedGrp.completion Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemiNormedGrp.instZeroHom CategoryTheory.Functor.obj	—	AddMonoidHom.map_zero
norm_incl_eq 📖	mathematical	—	Norm.norm SemiNormedGrp.carrier CategoryTheory.Functor.obj SemiNormedGrp SemiNormedGrp.instLargeCategory SemiNormedGrp.completion SeminormedAddCommGroup.toNorm SemiNormedGrp.str DFunLike.coe CategoryTheory.ConcreteCategory.hom NormedAddGroupHom NormedAddGroupHom.funLike SemiNormedGrp.instConcreteCategoryNormedAddGroupHomCarrier incl	—	UniformSpace.Completion.norm_coe

---

← Back to Index