hasPullback_assoc_symm — Mathlib

English

Symmetric version of pullback associativity under dual pullback assumptions.

Русский

Симметричная версия ассоциативности pullback при двойственных предпосылках.

LaTeX

$$$[HasPullback f_1 (g_3\circ f_4)]\; \Rightarrow \text{pullback assoc symm} $$$

Lean4

theorem hasPullback_assoc_symm [HasPullback f₁ (g₃ ≫ f₂)] : HasPullback (g₂ ≫ f₃) f₄ :=
  ⟨⟨⟨_, pullbackAssocSymmIsPullback f₁ f₂ f₃ f₄⟩⟩⟩

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