instIsTransLT — Mathlib

English

If LT is transitive on α, then LT on the dual αᵒᵈ is transitive as well.

Русский

Если отношение < транзитивно на α, то в дуальном порядке αᵒᵈ оно также транзитивно.

LaTeX

$$$ [\text{IsTrans}(α, LT.lt)] \Rightarrow [\text{IsTrans}(α^{\mathrm{op}}, LT.lt)] $$$

Lean4

instance instIsTransLT [LT α] [T : IsTrans α LT.lt] : IsTrans αᵒᵈ LT.lt where
  trans := fun _ _ _ hab hbc ↦ T.trans _ _ _ hbc hab

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