prodMap — Mathlib

English

The product of two affine maps corresponds to the product function: prod f g = Pi.prod f g.

Русский

Произведение двух отображений соответствует функции произведения: prod f g = Pi.prod f g.

LaTeX

$$$$\\text{prod}(f,g) = \\Pi\\text{.prod}(f,g).$$$$

Lean4

/-- `Prod.map` of two continuous affine maps. -/
@[simps toAffineMap]
def prodMap (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) : P₁ × P₃ →ᴬ[k] P₂ × P₄
    where
  __ := AffineMap.prodMap f g
  cont := by eta_expand; dsimp; fun_prop

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