congr_fun — Mathlib

English

If two morphisms are equal, then their values at any element are equal; i.e., equality is preserved by evaluation.

Русский

Если два отображения равны, то их значения на любом элементе совпадают.

LaTeX

$$$\\text{If } \\phi_1 = \\phi_2, \\text{ then } \\phi_1(x) = \\phi_2(x) \\text{ for all } x \\in A$$$

Lean4

protected theorem congr_fun {φ₁ φ₂ : A →ₐc[R] B} (H : φ₁ = φ₂) (x : A) : φ₁ x = φ₂ x :=
  DFunLike.congr_fun H x

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