gt — Mathlib · SciLib

English

WithTop α is trichotomous for > if α is trichotomous for >; follows by swapping the order.

Русский

WithTop α тричотомично по '>' если α тричотомично по '>' (перестановкой).

LaTeX

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

Lean4

instance _root_.WithBot.trichotomous.gt [Preorder α] [h : IsTrichotomous α (· > ·)] : IsTrichotomous (WithBot α) (· > ·)
    where trichotomous x y := by cases x <;> cases y <;> simp; simpa using trichotomous_of (· > ·) ..

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