isTrichotomous — Mathlib

English

If r is trichotomous on α, then the Shortlex order on List α is trichotomous.

Русский

Если r тричотомично на α, то порядок Shortlex на List α также тричотомичен.

LaTeX

$$$ \\text{IsTrichotomous }(\\text{List }\\alpha)(\\text{Shortlex } r) \\text{ follows from } IsTrichotomous(\\alpha,r).$$$

Lean4

instance isTrichotomous [IsTrichotomous α r] : IsTrichotomous (List α) (Shortlex r) :=
  ⟨(InvImage.isTrichotomous (by simp [Function.Injective])).trichotomous⟩

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