congr_fun₂ — Mathlib

English

Two bilinear maps are equal if they agree pointwise on all inputs; this is an extensionality principle for bilinear maps.

Русский

Два билинейных отображения равны, если они совпадают на всех входах, это экстенсионность билинейных отображений.

LaTeX

$$$$ f = g \Rightarrow (\forall m,n, f m n = g m n) $$$$

Lean4

theorem congr_fun₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x y) : f x y = g x y :=
  LinearMap.congr_fun (LinearMap.congr_fun h x) y

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