Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 22:45 1cbb31de

View on Github →

feat(analysis/normed_space/normed_group_hom): add lemmas (#7474) From LTE. Written by @PatrickMassot

depends on: #7459

Estimated changes

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem normed_group_hom.comp_range

added theorem normed_group_hom.incl_range

added theorem normed_group_hom.norm_incl

added theorem normed_group_hom.range_comp_incl_top