HomCompletion

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

Statistics

Metric	Count
Definitions toCompl, completion, extension, normedAddGroupHomCompletionHom	4
Theorems denseRange_toCompl, norm_toCompl, toCompl_apply, completion_add, completion_coe, completion_coe', completion_coe_to_fun, completion_comp, completion_def, completion_id, completion_neg, completion_sub, completion_toCompl, extension_coe, extension_coe_to_fun, extension_def, extension_unique, ker_completion, ker_le_ker_completion, norm_completion, zero_completion, normedAddGroupHomCompletionHom_apply	22
Total	26

NormedAddCommGroup

Definitions

Name	Category	Theorems
toCompl 📖	CompOp	6 math math: norm_toCompl, denseRange_toCompl, NormedAddGroupHom.ker_completion, NormedAddGroupHom.completion_toCompl, toCompl_apply, NormedAddGroupHom.ker_le_ker_completion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denseRange_toCompl 📖	mathematical	—	DenseRange UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace DFunLike.coe NormedAddGroupHom toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup NormedAddGroupHom.funLike toCompl	—	IsDenseInducing.dense UniformSpace.Completion.isDenseInducing_coe
norm_toCompl 📖	mathematical	—	Norm.norm UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm DFunLike.coe NormedAddGroupHom toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup NormedAddGroupHom.funLike toCompl	—	UniformSpace.Completion.norm_coe
toCompl_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup NormedAddGroupHom.funLike toCompl UniformSpace.Completion.coe'	—	—

NormedAddGroupHom

Definitions

Name	Category	Theorems
completion 📖	CompOp	15 math math: completion_def, zero_completion, norm_completion, completion_sub, completion_coe, completion_add, normedAddGroupHomCompletionHom_apply, completion_coe_to_fun, ker_completion, completion_toCompl, completion_neg, ker_le_ker_completion, completion_comp, SemiNormedGrp.completion_map, completion_id
extension 📖	CompOp	4 math math: extension_coe_to_fun, extension_coe, extension_unique, extension_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completion_add 📖	mathematical	—	completion NormedAddGroupHom add UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup	—	AddMonoidHom.map_add
completion_coe 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup funLike completion UniformSpace.Completion.coe'	—	UniformSpace.Completion.map_coe uniformContinuous
completion_coe' 📖	mathematical	—	UniformSpace.Completion.map PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe NormedAddGroupHom funLike UniformSpace.Completion.coe'	—	completion_coe
completion_coe_to_fun 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup funLike completion UniformSpace.Completion.map	—	—
completion_comp 📖	mathematical	—	comp UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup completion	—	ext coe_comp completion_def completion_coe_to_fun UniformSpace.Completion.map_comp uniformContinuous
completion_def 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup funLike completion UniformSpace.Completion.map	—	—
completion_id 📖	mathematical	—	completion id UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup	—	ext completion_def coe_id UniformSpace.Completion.map_id
completion_neg 📖	mathematical	—	completion NormedAddGroupHom neg UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup	—	map_neg AddMonoidHom.instAddMonoidHomClass
completion_sub 📖	mathematical	—	completion NormedAddGroupHom sub UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup	—	map_sub AddMonoidHom.instAddMonoidHomClass
completion_toCompl 📖	mathematical	—	comp UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup completion NormedAddCommGroup.toCompl	—	ext completion_coe'
extension_coe 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup funLike extension UniformSpace.Completion.coe'	—	AddMonoidHom.extension_coe SeminormedAddCommGroup.to_isUniformAddGroup continuous
extension_coe_to_fun 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup funLike extension UniformSpace.Completion.extension	—	—
extension_def 📖	mathematical	—	DFunLike.coe NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup funLike extension UniformSpace.Completion.coe' UniformSpace.Completion.extension	—	—
extension_unique 📖	mathematical	DFunLike.coe NormedAddGroupHom funLike UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup UniformSpace.Completion.coe'	extension	—	ext extension_coe_to_fun UniformSpace.Completion.extension_unique uniformContinuous
ker_completion 📖	mathematical	SurjectiveOnWith range	SetLike.coe AddSubgroup UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup AddSubgroup.instSetLike ker completion closure UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace SetLike.instMembership AddSubgroup.seminormedAddCommGroup comp NormedAddCommGroup.toCompl incl	—	le_antisymm SeminormedAddCommGroup.mem_closure_iff SurjectiveOnWith.exists_pos exists_pos_mul_lt Real.instIsStrictOrderedRing IsDenseInducing.dense UniformSpace.Completion.isDenseInducing_coe mem_range_self mem_ker map_sub toAddMonoidHomClass sub_eq_zero SeminormedAddCommGroup.to_isUniformAddGroup completion_coe' zero_sub norm_neg UniformSpace.Completion.norm_coe norm_completion le_opNorm mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt norm_nonneg UniformSpace.Completion.coe_sub sub_add norm_add_le add_lt_add_of_lt_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_le_add_right add_mul Distrib.rightDistribClass one_mul mul_assoc closure_minimal ker_le_ker_completion isClosed_ker
ker_le_ker_completion 📖	mathematical	—	AddSubgroup UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder range SetLike.instMembership AddSubgroup.instSetLike ker AddSubgroup.seminormedAddCommGroup comp NormedAddCommGroup.toCompl incl completion	—	completion_coe'
norm_completion 📖	mathematical	—	Norm.norm NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup hasOpNorm completion	—	le_antisymm ofLipschitz_norm_le SeminormedAddCommGroup.to_isUniformAddGroup continuous opNorm_nonneg opNorm_le_bound norm_nonneg completion_coe' UniformSpace.Completion.norm_coe le_opNorm
zero_completion 📖	mathematical	—	completion NormedAddGroupHom zero UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup	—	AddMonoidHom.map_zero

(root)

Definitions

Name	Category	Theorems
normedAddGroupHomCompletionHom 📖	CompOp	1 math math: normedAddGroupHomCompletionHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normedAddGroupHomCompletionHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom NormedAddGroupHom UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.Completion.instNormedAddCommGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddGroupHom.toSeminormedAddCommGroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace NormedAddGroupHom.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike normedAddGroupHomCompletionHom NormedAddGroupHom.completion	—	—

---

← Back to Index