toIsometry_injective — Mathlib

English

The map Hom.toIsometry : Hom V W → Isometry(V.form, W.form) is injective in QuadraticModuleCat.

Русский

Отображение Hom.toIsometry: Морфизмы V ⟶ W в изометрии является инъективным в QuadraticModuleCat.

LaTeX

$$$ \operatorname{Injective}(\text{Hom}.\text{toIsometry}) $$$

Lean4

theorem toIsometry_injective (V W : QuadraticModuleCat.{v} R) : Function.Injective (Hom.toIsometry : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

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