linearOrder — Mathlib

English

If α has a PartialOrder and is totally ordered, then there is a linear order on AsLinearOrder α extending the given order, with decidable ≤.

Русский

Если у α задан частичный порядок и он линейно упорядочен, то на типе AsLinearOrder α существует линейный порядок, расширяющий данный порядок, с разрешимой связкой ≤.

LaTeX

$$$\text{LinearOrder}(\mathrm{AsLinearOrder}\,\alpha)$$$

Lean4

noncomputable instance linearOrder [PartialOrder α] [IsTotal α (· ≤ ·)] : LinearOrder (AsLinearOrder α)
    where
  __ := inferInstanceAs (PartialOrder α)
  le_total := @total_of α (· ≤ ·) _
  toDecidableLE := Classical.decRel _

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