toPullback_cylinder — Mathlib

English

For i, j in the cylinder of f and g, and any k in I1, the toPullback morphism equals the first projection of the pullback.

Русский

Для i, j в цилиндре f и g и любого k в I1, отображение toPullback равно первой проекции на вытянутой диагонали.

LaTeX

$$$ (\\,\\text{cylinder } f\\; g\\,).toPullback\\;k = \\text{pullback}.fst\\ _\\ _ $$$

Lean4

theorem toPullback_cylinder {i j : (cylinder f g).I₀} (k : (cylinder f g).I₁ i j) :
    (cylinder f g).toPullback k = pullback.fst _ _ := by apply pullback.hom_ext <;> simp [toPullback]

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