coe_linearMap_injective — Mathlib

English

If two coalgebra morphisms agree on every input, they are equal

Русский

Если два коалгоморфизма совпадают на каждом входе, они равны

LaTeX

$$$$ \forall x, \phi_1 x = \phi_2 x \Rightarrow \phi_1 = \phi_2 $$$$

Lean4

theorem coe_linearMap_injective : Function.Injective ((↑) : (A →ₗc[R] B) → A →ₗ[R] B) := fun φ₁ φ₂ H =>
  coe_fn_injective <| show ((φ₁ : A →ₗ[R] B) : A → B) = ((φ₂ : A →ₗ[R] B) : A → B) from congr_arg _ H

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