hasPushout_assoc_symm — Mathlib

English

If there are pushouts for g1,g2 and for g3,g4, then there is a pushout for g3 ≫ f2 and g4, i.e., a symmetric rearrangement of pushouts exists.

Русский

Если существуют приведенные к сумме частичные сцепления (pushouts) g1,g2 и g3,g4, то существует pushout для g3 ≫ f2 и g4; симметричное переразмещение существует.

LaTeX

$$$\\text{HasPushout } g_3 (g_2 \\!\\gg g_1) \\;\\vdash\\; \\text{HasPushout } (g_3 \\circ f_2) g_4$$$

Lean4

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

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