Documentation

TauCeti.Order.SuccPred.Sum

Successors and predecessors in lexicographic sums #

In the lexicographic sum α ⊕ₗ β, every element of α lies below every element of β. When α has no maximal element, the successor of an element of either summand is its successor inside that summand, so α ⊕ₗ β is a successor order. Dually, when β has no minimal element, α ⊕ₗ β is a predecessor order with predecessors computed inside the summands. For example ℤ ⊕ₗ ℤ, two copies of the integers one after the other, is a successor and predecessor order without endpoints that is not isomorphic to ℤ.

source
@[instance_reducible]
instance Sum.Lex.succOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SuccOrder α] [SuccOrder β] [NoMaxOrder α] :
SuccOrder (α ⊕ₗ β)

When α has no maximal element, successors in α ⊕ₗ β are computed inside the summands.

source
@[simp]
theorem Sum.Lex.succ_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SuccOrder α] [SuccOrder β] [NoMaxOrder α] (a : α) :
Order.succ (toLex (inl a)) = toLex (inl (Order.succ a))

The successor of an element of the left summand is its successor there.

source
@[simp]
theorem Sum.Lex.succ_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SuccOrder α] [SuccOrder β] [NoMaxOrder α] (b : β) :
Order.succ (toLex (inr b)) = toLex (inr (Order.succ b))

The successor of an element of the right summand is its successor there.

source
@[instance_reducible]
instance Sum.Lex.predOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [PredOrder α] [PredOrder β] [NoMinOrder β] :
PredOrder (α ⊕ₗ β)

When β has no minimal element, predecessors in α ⊕ₗ β are computed inside the summands.

source
@[simp]
theorem Sum.Lex.pred_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [PredOrder α] [PredOrder β] [NoMinOrder β] (a : α) :
Order.pred (toLex (inl a)) = toLex (inl (Order.pred a))

The predecessor of an element of the left summand is its predecessor there.

source
@[simp]
theorem Sum.Lex.pred_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [PredOrder α] [PredOrder β] [NoMinOrder β] (b : β) :
Order.pred (toLex (inr b)) = toLex (inr (Order.pred b))

The predecessor of an element of the right summand is its predecessor there.