∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {f : NormedAddGroupHom M N},
  Function.Surjective ⇑f → (∀ (x : M), ‖f x‖ = sInf ((fun m => ‖x + m‖) '' ↑f.ker)) → f.IsQuotient