pullback_singleton — Mathlib

English

The pullback arrows of f with the presieve singleton g is the singleton of the pullback projection snd g f.

Русский

Стрелы вытяжки (pullback) f и предсистемы-одиночки g равны одиночке стрелки вытяжки snd g f.

LaTeX

$$$\\mathrm{pullbackArrows}(f,\\mathrm{singleton}(g)) = \\mathrm{singleton}\\big(\\mathrm{pullback}.snd\\, g\\, f\\big)$$$

Lean4

theorem pullback_singleton (g : Z ⟶ X) [HasPullback g f] :
    pullbackArrows f (singleton g) = singleton (pullback.snd g f) :=
  by
  funext W
  ext h
  constructor
  · rintro ⟨W, _, _, _⟩
    exact singleton.mk
  · rintro ⟨_⟩
    exact pullbackArrows.mk Z g singleton.mk

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