iso_isometry_of_normNoninc — Mathlib

English

If i is an isomorphism with both directions normNoninc, then i.hom is an isometry.

Русский

Если i — изоморфизм и оба направления имеют NormNoninc, то i.hom является изометрией.

LaTeX

$$$ \text{Isometry}(i.hom) $ given $ i.hom, (i.inv).NormNoninc, (i.hom).NormNoninc $$$

Lean4

theorem iso_isometry_of_normNoninc {V W : SemiNormedGrp} (i : V ≅ W) (h1 : i.hom.hom.NormNoninc)
    (h2 : i.inv.hom.NormNoninc) : Isometry i.hom :=
  by
  apply AddMonoidHomClass.isometry_of_norm
  intro v
  apply le_antisymm (h1 v)
  calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := h2 _

Похожие утверждения