coe_injective — Mathlib

English

There is a canonical EquivLike structure on the type E ≃ₛₗᵢ[σ] E'.

Русский

Существует каноническая структура EquivLike на множество линейно изометрических эквивалентностей между E и E'.

LaTeX

$$$\\text{EquivLike }(E \\simeq_{\\mathrm{LI}} E')$$$

Lean4

theorem coe_injective : @Function.Injective (E ≃ₛₗᵢ[σ₁₂] E₂) (E → E₂) (↑) :=
  DFunLike.coe_injective

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