prodMap_apply — Mathlib

English

For affine maps f and g as above, the product map acts coordinatewise: (f.prodMap g)(p1, p3) = (f(p1), g(p3)).

Русский

Для аффинных отображений f и g произведение отображений действует по координатам: (f.prodMap g)(p1, p3) = (f(p1), g(p3)).

LaTeX

$$$(f \mathrm{prodMap} g)(x) = (f(x_1), g(x_2))$ для любого $x=(x_1,x_2)\in P_1\times P_3$.$$

Lean4

@[simp]
theorem prodMap_apply (f : P1 →ᵃ[k] P2) (g : P3 →ᵃ[k] P4) (x) : f.prodMap g x = (f x.1, g x.2) :=
  rfl

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