coe_inj — Mathlib

English

The map sending f to its coefficient function (f a b) is injective: if (f = g) holds iff their coefficients agree.

Русский

Отображение из IncidenceAlgebra в функцию-коэффициентов инъективно: если коэффициенты совпадают, то функции равны.

LaTeX

$$$ (f : \alpha \to \alpha \to 𝕜) = g \;\iff\; f = g $$$

Lean4

theorem coe_inj {f g : IncidenceAlgebra 𝕜 α} : (f : α → α → 𝕜) = g ↔ f = g :=
  DFunLike.coe_injective.eq_iff

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