instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq

English

Under decidability assumptions, the subtype of a flag inherits a linear order.

Русский

При условиях разрешимости подтип флага наследует линейный порядок.

LaTeX

$$$[DecidableLE α] \\rightarrow [DecidableLT α] \\rightarrow [DecidableEq α] \\rightarrow (s : Flag α) \\rightarrow LinearOrder (Subtype (\\\\lambda x \\in s x))$$$

Lean4

instance [DecidableLE α] [DecidableLT α] [DecidableEq α] (s : Flag α) : LinearOrder s :=
  { Subtype.partialOrder _ with
    le_total := fun a b => s.le_or_le a.2 b.2
    toDecidableLE := Subtype.decidableLE
    toDecidableLT := Subtype.decidableLT
    toDecidableEq := Subtype.instDecidableEq }

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