From 3d9992651f11f67c4e48c0a0e7c4bacfa3328ca0 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Sat, 16 Oct 2021 18:01:06 +0000
Subject: [PATCH] feat(analysis/normed/group/SemiNormedGroup): add
 iso_isometry_of_norm_noninc (#9710)

From LTE.
---
 src/analysis/normed/group/SemiNormedGroup.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/analysis/normed/group/SemiNormedGroup.lean b/src/analysis/normed/group/SemiNormedGroup.lean
index ac57053daecba..fb0d9b02facab 100644
--- a/src/analysis/normed/group/SemiNormedGroup.lean
+++ b/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
 
 /--