coe_fn_injective — Mathlib

English

The map that sends a bialg morphism to its underlying function is injective: if two morphisms have the same underlying function, they are equal.

Русский

Отображение, отправляющее гомоморфизм биналг Hom на соответствующее ему отображение, инъективно: если две функции совпадают, то сами гомоморфизмы равны.

LaTeX

$$$\\forall \\phi_1, \\phi_2 : A \\to_{\\!R} B,\\ (\\phi_1 : A \\to B) = \\phi_2 \\ \\Rightarrow\\ \\phi_1 = \\phi_2$$$

Lean4

theorem coe_fn_injective : @Function.Injective (A →ₐc[R] B) (A → B) (↑) :=
  DFunLike.coe_injective

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