English
Let f: X → Y and g: Y → Z be morphisms with HomIsOver f S and HomIsOver g S, and with appropriate OverClass and IsOverTower conditions for S, S'. Then HomIsOver f S'.
Русский
Пусть f: X → Y и g: Y → Z — морфизмы, для которых выполняются HomIsOver f S и HomIsOver g S, и выполнены соответствующие условия OverClass и IsOverTower для S и S'. Тогда HomIsOver f S'.
LaTeX
$$$\forall f:X\to Y, g:Y\to Z, S,S' : \mathcal C,\ [OverClass X S], [OverClass Y S], [OverClass Z S], [OverClass X S'], [OverClass Y S'], [OverClass S S'], [IsOverTower X S S'], [IsOverTower Y S S'], [HomIsOver f S] \Rightarrow [HomIsOver f S']$$$
Lean4
theorem homIsOver_of_isOverTower [OverClass X S] [OverClass X S'] [OverClass Y S] [OverClass Y S'] [OverClass S S']
[IsOverTower X S S'] [IsOverTower Y S S'] [HomIsOver f S] : HomIsOver f S' :=
by
constructor
rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]
