hasPushout_assoc — Mathlib

English

The pushout of composed morphisms is associative up to a canonical isomorphism under suitable pushout hypotheses.

Русский

Слияние (pushout) композиции морфизмов является ассоциативным до канонического изоморфизма при подходящих условиях.

LaTeX

$$$[HasPushout g_1 g_2]\,[HasPushout g_3 g_4] \Rightarrow \text{HasPushout } g_1 (g_2 \circ f_3)$$$

Lean4

theorem hasPushout_assoc [HasPushout (g₃ ≫ f₂) g₄] : HasPushout g₁ (g₂ ≫ f₃) :=
  ⟨⟨⟨_, pushoutAssocIsPushout g₁ g₂ g₃ g₄⟩⟩⟩

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