t_fst_snd — Mathlib

English

Similarly, the composition t with snd then snd again equals the composition with fst then fst, encoding the same symmetry property in the alternative projection.

Русский

Аналогично, композиция t с snd и повторное snd дают то же, что fst затем fst, отражая симметрию в другой проекции.

LaTeX

$$$t 𝒰 f g i j ≫ pullback.snd _ _ ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.fst _ _$$$

Lean4

@[simp, reassoc]
theorem t_fst_snd (i j : 𝒰.I₀) :
    t 𝒰 f g i j ≫ pullback.fst _ _ ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.snd _ _ := by
  simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_snd, pullback.lift_snd,
    Category.comp_id, pullbackAssoc_inv_snd, pullbackSymmetry_hom_comp_snd_assoc]

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