instIsTransLE — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance instIsTransLE [LE α] [T : IsTrans α LE.le] : IsTrans αᵒᵈ LE.le where
  trans := fun _ _ _ hab hbc ↦ T.trans _ _ _ hbc hab

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