coe_fn_inj — Mathlib

English

Two morphisms are equal if and only if their underlying functions are equal.

Русский

Два гомоморфизма равны тогда и только тогда, когда их соответствующие функции равны.

LaTeX

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

Lean4

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

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