feat(analysis/normed/group/SemiNormedGroup): add iso_isometry_of_norm…

…_noninc (#9710)

From LTE.

src/analysis/normed/group/SemiNormedGroup.lean

@@ -55,6 +55,17 @@ instance has_zero_object : limits.has_zero_object SemiNormedGroup.{u} :=
   { default := 0,
     uniq := λ f, by ext } }
 
+lemma iso_isometry_of_norm_noninc {V W : SemiNormedGroup} (i : V ≅ W)
+  (h1 : i.hom.norm_noninc) (h2 : i.inv.norm_noninc) :
+  isometry i.hom :=
+begin
+  apply normed_group_hom.isometry_of_norm,
+  intro v,
+  apply le_antisymm (h1 v),
+  calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [coe_hom_inv_id]
+  ... ≤ ∥i.hom v∥ : h2 _,
+end
+
 end SemiNormedGroup
 
 /--