vert_comp — Mathlib

English

The vertical composition of two commuting squares is again a commuting square.

Русский

Вертикальное соединение двух коммутативных квадратов снова образует коммутативный квадрат.

LaTeX

$$$CommSq f (g \gg g') (h \gg h') i'$, given $hsq_1$ and $hsq_2$$$

Lean4

/-- The vertical composition of two commutative squares as below is a commutative square.
```
  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z
  |          |
  g'         h'
  |          |
  v          v
  Y'---i'--> Z'

```
-/
theorem vert_comp {W X Y Y' Z Z' : C} {f : W ⟶ X} {g : W ⟶ Y} {g' : Y ⟶ Y'} {h : X ⟶ Z} {h' : Z ⟶ Z'} {i : Y ⟶ Z}
    {i' : Y' ⟶ Z'} (hsq₁ : CommSq f g h i) (hsq₂ : CommSq i g' h' i') : CommSq f (g ≫ g') (h ≫ h') i' :=
  flip (horiz_comp (flip hsq₁) (flip hsq₂))

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