lt — Mathlib · SciLib

English

WithBot α is trichotomous for < provided α is a Preorder and IsTrichotomous α (<).

Русский

WithBot α тричотомично по '<' если α имеет предорядок и IsTrichotomous α(<).

LaTeX

$$$\\operatorname{IsTrichotomous}(\\mathrm{WithBot}\\,\\alpha, <)$ given Preorder α and IsTrichotomous α(<).$$

Lean4

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

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