prodToProdTop_map — Mathlib

English

On the pair (p0,p1) between objects, the map equals Path.Homotopic.prod p0 p1.

Русский

На паре путей (p0,p1) между объектами отображение равно Path.Homotopic.prod p0 p1.

LaTeX

$$$$ (prodToProdTop A B).map (X := (x_0,y_0)) (Y := (x_1,y_1)) (p_0,p_1) = Path.Homotopic.prod p_0 p_1 $$$$

Lean4

theorem prodToProdTop_map {x₀ x₁ : πₓ A} {y₀ y₁ : πₓ B} (p₀ : x₀ ⟶ x₁) (p₁ : y₀ ⟶ y₁) :
    (prodToProdTop A B).map (X := (x₀, y₀)) (Y := (x₁, y₁)) (p₀, p₁) = Path.Homotopic.prod p₀ p₁ :=
  rfl

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