pullbackSnd — Mathlib

English

The second projection from the pullback pb(f,g) is the projection onto the second coordinate.

Русский

Вторая проекция из pullback pb(f,g) проецирует на вторую координату.

LaTeX

$$$\\mathrm{pullbackSnd}(f,g) : \\mathrm{TopCat.of}\\{ p:(X×Y)\\mid f p.1 = g p.2\\} \\to Y$$$

Lean4

/-- The second projection from the pullback. -/
abbrev pullbackSnd (f : X ⟶ Z) (g : Y ⟶ Z) : TopCat.of { p : X × Y // f p.1 = g p.2 } ⟶ Y :=
  ofHom ⟨Prod.snd ∘ Subtype.val, by fun_prop⟩

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