projRight_map — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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