prod — Mathlib

English

The product of two continuous affine maps is again a continuous affine map: given f: P₁ →ᴬ[k] P₂ and g: P₁ →ᴬ[k] P₃, their product is a map P₁ →ᴬ[k] P₂ × P₃.

Русский

Произведение двух непрерывных аффинных отображений снова является непрерывным аффинным отображением: f: P₁ →ᴬ[k] P₂ и g: P₁ →ᴬ[k] P₃ дают отображение P₁ →ᴬ[k] P₂ × P₃.

LaTeX

$$$$\\text{prod}(f,g)\\in P₁ →ᴬ[k] (P₂ \\times P₃).$$$$

Lean4

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

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