coe_fn_injective — Mathlib

English

The map sending a coalgebra morphism to its underlying function is injective: if two morphisms have the same action on every input, they are equal

Русский

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

LaTeX

$$$$ ([\phi_1], [\phi_2] : \text{CoalgHom } R A B) \, (\phi_1|_A = \phi_2|_A) \Rightarrow \phi_1 = \phi_2 $$$$

Lean4

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

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