[Merged by Bors] - feat(analysis/normed_space/normed_group_hom): add lemmas

src/analysis/normed_space/normed_group_hom.lean

@@ -411,6 +411,9 @@ variables [semi_normed_group V] [semi_normed_group W] [semi_normed_group V₁] [
   map_add' := λ v w, add_subgroup.coe_add _ _ _,
   bound' := ⟨1, λ v, by { rw [one_mul], refl }⟩ }
 
+lemma norm_incl {V' : add_subgroup V} (x : V') : ∥incl _ x∥ = ∥x∥ :=
+rfl
+
 /-!### Kernel -/
 section kernels
 variables (f : normed_group_hom V₁ V₂) (g : normed_group_hom V₂ V₃)
@@ -458,6 +461,22 @@ def range : add_subgroup V₂ := f.to_add_monoid_hom.range
 lemma mem_range (v : V₂) : v ∈ f.range ↔ ∃ w, f w = v :=
 by { rw [range, add_monoid_hom.mem_range], refl }
 
+lemma comp_range : (g.comp f).range = add_subgroup.map g.to_add_monoid_hom f.range :=
+begin
+  erw add_monoid_hom.map_range,
+  refl,
+end
+
+lemma incl_range (s : add_subgroup V₁) : (incl s).range = s :=
+begin
+  ext x,
+  exact ⟨λ ⟨y, hy⟩, by { rw ← hy; simp }, λ hx, ⟨⟨x, hx⟩, by simp⟩⟩,
+end
+
+@[simp]
+lemma range_comp_incl_top : (f.comp (incl (⊤ : add_subgroup V₁))).range = f.range :=
+by simpa [comp_range, incl_range, ← add_monoid_hom.range_eq_map]
+
 end range
 
 variables {f : normed_group_hom V W}