iso_isometry — Mathlib

English

Any isomorphism i: V ≅ W in SemiNormedGrp₁ induces an isometry on the forward map i.hom.

Русский

Любой изоморфизм i: V ≅ W в SemiNormedGrp₁ порождает изометрию на отображении i.hom.

LaTeX

$$Isometry(i.hom)$$

Lean4

theorem iso_isometry {V W : SemiNormedGrp₁} (i : V ≅ W) : Isometry i.hom :=
  by
  change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)
  refine AddMonoidHomClass.isometry_of_norm _ ?_
  intro v
  apply le_antisymm (i.hom.2 v)
  calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := i.inv.2 _

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