Documentation

BourbakiLean2.Order.Lex

source
def Lex (ι : Type u_1) (α : ι → Type u_2) :
Type (max u_1 u_2)
Equations
  • Lex ι α = ((i : ι) → α i)
Instances For
    source
    instance instPartialOrderLexOfTotalOrder {ι : Type u_1} {α : ι → Type u_2} [TotalOrder ι] [(i : ι) → PartialOrder (α i)] :
    PartialOrder (Lex ι α)
    Equations
    source
    instance instTotalOrderLexOfWellOrder {ι : Type u_1} {α : ι → Type u_2} [WellOrder ι] [(i : ι) → TotalOrder (α i)] :
    TotalOrder (Lex ι α)
    Equations