gt — Mathlib · SciLib

English

If α is trichotomous with respect to >, then WithTop α is trichotomous with respect to >.

Русский

Если у α тричотомично по отношению к '>', то WithTop α также тричотомично по '>'.

LaTeX

$$$\\operatorname{IsTrichotomous}(\\mathrm{WithTop}\\,\\alpha, >)$ provided IsTrichotomous α(>).$$

Lean4

instance gt [Preorder α] [IsTrichotomous α (· > ·)] : IsTrichotomous (WithTop α) (· > ·) :=
  have : IsTrichotomous α (· < ·) := .swap _;
  .swap _

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