instHomIsOverOfIsOverTower_1 — Mathlib

English

Assume OverClass X S, OverClass X S', OverClass Y S, OverClass Y S', OverClass S S', IsOverTower X S S', 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 [OverClass X S] [OverClass X S'] [CanonicallyOverClass 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'

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