projLeft_map — Mathlib

English

For any x0, x1 and p, the map induced by projLeft A B agrees with Path.Homotopic.projLeft p.

Русский

Для любых x0, x1 и p отображение, индуцируемое projLeft A B, совпадает с Path.Homotopic.projLeft p.

LaTeX

$$$$ (projLeft A B).map p = Path.Homotopic.projLeft p $$$$

Lean4

@[simp]
theorem projLeft_map (x₀ x₁ : πₓ (TopCat.of (A × B))) (p : x₀ ⟶ x₁) :
    (projLeft A B).map p = Path.Homotopic.projLeft p :=
  rfl

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