coe_fn_inj — Mathlib

English

If φ1 and φ2 are R-algebra homomorphisms, then equality of their functions implies equality of the homomorphisms: (φ1 : A → B) = (φ2 : A → B) iff φ1 = φ2.

Русский

Если φ1 и φ2 — R-алгоморфизмы, то равенство их функций означает равенство самих гомоморфизмов: (φ1 : A → B) = (φ2 : A → B) тогда и только тогда, когда φ1 = φ2.

LaTeX

$$$(\\phi_1 : A \\to B) = (\\phi_2 : A \\to B) \\;\\Leftrightarrow\\; \\phi_1 = \\phi_2$$$

Lean4

theorem coe_fn_inj {φ₁ φ₂ : A →ₐ[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂ :=
  DFunLike.coe_fn_eq

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