lt — Mathlib · SciLib

English

If α is a Preorder and IsTrichotomous α (<), then WithTop α is IsTrichotomous for <.

Русский

Если у α есть предпорядок и IsTrichotomous α(<), то WithTop α сохраняет тричотомичность по '<'.

LaTeX

$$$\\text{IsTrichotomous}(\\mathrm{WithTop}\\,\\alpha, <)$$$

Lean4

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

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