pullbackAssoc_inv_snd — Mathlib

English

Another variant of the inverse-pullback associativity with the second projection.

Русский

Другой вариант обратной ассоциативности pullback через вторую проекцию.

LaTeX

$$$\text{pullbackAssoc_inv_snd}$ (second form)$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAssoc_inv_snd [HasPullback ((pullback.snd _ _ : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst _ _ : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.snd _ _ := by
  rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]

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