congr_fun — Mathlib

English

If two algebra homomorphisms φ1 and φ2 are equal, then they agree on every input x: φ1 x = φ2 x for all x.

Русский

Если два алгоморфизма φ1 и φ2 равны, то они совпадают на каждом элементе: φ1 x = φ2 x для всех x.

LaTeX

$$$\\phi_1 = \\phi_2 \\Rightarrow ∀ x, \\; φ_1 x = φ_2 x$$$

Lean4

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

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