coe_injective — Mathlib

English

The coercion from multilinear maps to functions is injective: if f and g have the same action as functions, then f = g.

Русский

Встраивание из много линейного отображения в функции инъективно: если f и g действуют одинаково на всех входах, то f = g.

LaTeX

$$$ (\forall x, f x = g x) \Rightarrow f = g $$$

Lean4

theorem coe_injective : Injective ((↑) : MultilinearMap R M₁ M₂ → (∀ i, M₁ i) → M₂) :=
  DFunLike.coe_injective

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