projRight — Mathlib

English

The induced map from π_x of a product to π_x B is given by the right projection.

Русский

Индуцированное отображение из π_x произведения в π_x B задаётся правым проецированием.

LaTeX

$$$$ \\text{projRight } A B : \\pi_x(A\\times B) \\to \\pi_x B $$$$

Lean4

/-- The induced map of the right projection map X × Y → Y -/
def projRight : πₓ (TopCat.of (A × B)) ⥤ πₓ B :=
  πₘ (TopCat.ofHom ⟨_, continuous_snd⟩)

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