coe_prodMap — Mathlib

English

Let f: P1 →ᵃ[k] P2 and g: P3 →ᵃ[k] P4 be affine maps. Then the product map f.prodMap g: P1 × P3 → P2 × P4 acts by (p1, p3) ↦ (f(p1), g(p3)). Equivalently, (f.prodMap g) = Prod.map f g as functions.

Русский

Пусть f: P1 →ᵃ[k] P2 и g: P3 →ᵃ[k] P4 — аффинные отображения. Тогда произведение отображений f.prodMap g: P1 × P3 → P2 × P4 действует по правилу (p1, p3) ↦ (f(p1), g(p3)). Эквивалентно, (f.prodMap g) = Prod.map f g как функции.

LaTeX

$$$ (f \mathrm{ prodMap } g)(p_1,p_3) = (f(p_1), g(p_3)) \quad\text{for all } p_1 \in P_1, p_3 \in P_3.$$$

Lean4

theorem coe_prodMap (f : P1 →ᵃ[k] P2) (g : P3 →ᵃ[k] P4) : ⇑(f.prodMap g) = Prod.map f g :=
  rfl

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