toLinearIsometry_injective — Mathlib

English

The map sending a LinearIsometryEquiv to its toLinearIsometry is injective.

Русский

Карта, отправляющая LinearIsometryEquiv в его toLinearIsometry, инъективна.

LaTeX

$$$\\mathrm{toLinearIsometry\_inj}: (E \\simeq_{\\mathrm{LI}} E') \\to (E \\to E')$ is injective$$

Lean4

theorem toLinearIsometry_injective : Function.Injective (toLinearIsometry : _ → E →ₛₗᵢ[σ₁₂] E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toLinearIsometry = _)

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