Commit 2023-03-12 19:12 db9f3412

View on Github →

feat: port Analysis.Normed.Group.HomCompletion (#2818)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Group/Hom.lean

modified theorem NormedAddGroupHom.mem_range

added def NormedAddGroupHom.ofLipschitz

added theorem NormedAddGroupHom.ofLipschitz_norm_le

Created Mathlib/Analysis/Normed/Group/HomCompletion.lean

added theorem NormedAddCommGroup.denseRange_toCompl

added theorem NormedAddCommGroup.norm_toCompl

added def NormedAddCommGroup.toCompl

added def NormedAddGroupHom.completion

added theorem NormedAddGroupHom.completion_add

added theorem NormedAddGroupHom.completion_coe'

added theorem NormedAddGroupHom.completion_coe

added theorem NormedAddGroupHom.completion_coe_to_fun

added theorem NormedAddGroupHom.completion_comp

added theorem NormedAddGroupHom.completion_def

added theorem NormedAddGroupHom.completion_id

added theorem NormedAddGroupHom.completion_neg

added theorem NormedAddGroupHom.completion_sub

added theorem NormedAddGroupHom.completion_toCompl

added def NormedAddGroupHom.extension

added theorem NormedAddGroupHom.extension_coe

added theorem NormedAddGroupHom.extension_coe_to_fun

added theorem NormedAddGroupHom.extension_def

added theorem NormedAddGroupHom.extension_unique

added theorem NormedAddGroupHom.ker_completion

added theorem NormedAddGroupHom.ker_le_ker_completion

added theorem NormedAddGroupHom.norm_completion

added theorem NormedAddGroupHom.zero_completion

added def normedAddGroupHomCompletionHom

Modified Mathlib/Topology/MetricSpace/Completion.lean

added theorem Isometry.completion_extension

added theorem Isometry.completion_map

added theorem LipschitzWith.completion_extension

added theorem LipschitzWith.completion_map

Modified Mathlib/Topology/UniformSpace/Completion.lean