coeFn_injective — Mathlib

English

The map sending a continuous σ12-semilinear map to its underlying function is injective.

Русский

Карта, отправляющая непрерывное σ12-семилинейное отображение в его базовую функцию, инъективна.

LaTeX

$$$\text{Injective} (\, f \mapsto f\,)$ on the set of ContinuousLinearMap$$

Lean4

theorem coeFn_injective : @Function.Injective (M₁ →SL[σ₁₂] M₂) (M₁ → M₂) (↑) :=
  DFunLike.coe_injective

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