t_snd — Mathlib

English

Given a triple T = (x,y,h) describing a point x in X, y in Y mapping to s in S with compatibility h, there exists t in the pullback X ×_S Y lying over x and y.

Русский

Для тройки T = (x,y, h) описывающей точку x в X, y в Y над s в S, существует t в произведении X ×_S Y над x и y.

LaTeX

$$$\exists t:\; (pullback.fst f g).base t = x \land (pullback.snd f g).base t = y$$$

Lean4

@[simp, reassoc]
theorem t_snd (i j : 𝒰.I₀) : t 𝒰 f g i j ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.fst _ _ := by
  simp only [t, Category.assoc, pullbackSymmetry_hom_comp_snd, pullbackAssoc_hom_fst, pullback.lift_fst_assoc,
    pullbackSymmetry_hom_comp_fst, pullbackAssoc_inv_fst_snd, pullbackSymmetry_hom_comp_snd_assoc]

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