Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-18 16:41 71c203a9

View on Github →

feat(analysis/normed/group/SemiNormedGroup/completion): add SemiNormedGroup.Completion (#9788) From LTE.

Estimated changes

Created src/analysis/normed/group/SemiNormedGroup/completion.lean

added def SemiNormedGroup.Completion.incl

added def SemiNormedGroup.Completion.lift

added theorem SemiNormedGroup.Completion.lift_comp_incl

added theorem SemiNormedGroup.Completion.lift_unique

added def SemiNormedGroup.Completion.map_hom

added theorem SemiNormedGroup.Completion.map_norm_noninc

added theorem SemiNormedGroup.Completion.map_zero

added theorem SemiNormedGroup.Completion.norm_incl_eq

added def SemiNormedGroup.Completion

Modified src/analysis/normed/group/hom_completion.lean

added def normed_group_hom.extension

added theorem normed_group_hom.extension_coe

added theorem normed_group_hom.extension_coe_to_fun

added theorem normed_group_hom.extension_def

added theorem normed_group_hom.extension_unique