instTransIsBigOTVSIsLittleOTVS — Mathlib

English

Instance asserting that transitivity from IsBigOTVS to IsLittleOTVS holds

Русский

Экземпляр, что транситивность IsBigOTVS к IsLittleOTVS выполняется

LaTeX

$$instTransIsBigOTVSIsLittleOTVS: Trans (IsBigOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l)$$

Lean4

instance instTransIsBigOTVSIsLittleOTVS :
    @Trans (α → E) (α → F) (α → G) (IsBigOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) where
  trans := IsBigOTVS.trans_isLittleOTVS

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