instHomIsOverOfIsOverTower — Mathlib

English

If there is an OverClass X S, and OverClass X S', OverClass Y S, OverClass Y S', and OverClass S S', with IsOverTower X S S' and IsOverTower Y S S', and HomIsOver f S, then HomIsOver f S'.

Русский

Пусть существуют 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'.

LaTeX

$$$[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] \Rightarrow HomIsOver f S'$$

Lean4

instance [CanonicallyOverClass 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' :=
  homIsOver_of_isOverTower f S S'

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