Orders on a sum type #
This file defines the disjoint sum and the linear (aka lexicographic) sum of two orders and
provides relation instances for Sum.LiftRel
and Sum.Lex
.
We declare the disjoint sum of orders as the default set of instances. The linear order goes on a type synonym.
Main declarations #
Sum.LE
,Sum.LT
: Disjoint sum of orders.Sum.Lex.LE
,Sum.Lex.LT
: Lexicographic/linear sum of orders.
Notation #
α ⊕ₗ β
: The linear sum ofα
andβ
.
Unbundled relation classes #
instance
Sum.instIsAntisymmLiftRel
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[IsAntisymm α r]
[IsAntisymm β s]
:
IsAntisymm (α ⊕ β) (LiftRel r s)
instance
Sum.instIsAntisymmLex
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[IsAntisymm α r]
[IsAntisymm β s]
:
IsAntisymm (α ⊕ β) (Lex r s)
instance
Sum.instIsTrichotomousLex
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[IsTrichotomous α r]
[IsTrichotomous β s]
:
IsTrichotomous (α ⊕ β) (Lex r s)
instance
Sum.instIsWellOrderLex
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[IsWellOrder α r]
[IsWellOrder β s]
:
IsWellOrder (α ⊕ β) (Lex r s)
Disjoint sum of two orders #
Equations
- Sum.instLESum = { le := Sum.LiftRel (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2 }
Equations
- Sum.instLTSum = { lt := Sum.LiftRel (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2 }
Equations
- Sum.instPreorderSum = { toLE := Sum.instLESum, toLT := Sum.instLTSum, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }
instance
Sum.instPartialOrder
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[PartialOrder β]
:
PartialOrder (α ⊕ β)
Equations
- Sum.instPartialOrder = { toPreorder := Sum.instPreorderSum, le_antisymm := ⋯ }
instance
Sum.noMinOrder
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[NoMinOrder α]
[NoMinOrder β]
:
NoMinOrder (α ⊕ β)
instance
Sum.noMaxOrder
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[NoMaxOrder α]
[NoMaxOrder β]
:
NoMaxOrder (α ⊕ β)
@[simp]
@[simp]
instance
Sum.denselyOrdered
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[DenselyOrdered α]
[DenselyOrdered β]
:
DenselyOrdered (α ⊕ β)
@[simp]
Linear sum of two orders #
The linear sum of two orders
Equations
- Sum.Lex.«term_⊕ₗ_» = Lean.ParserDescr.trailingNode `Sum.Lex.«term_⊕ₗ_» 30 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ₗ ") (Lean.ParserDescr.cat `term 29))
Instances For
instance
Sum.Lex.preorder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
:
Preorder (_root_.Lex (α ⊕ β))
Equations
- Sum.Lex.preorder = { toLE := Sum.Lex.LE, toLT := Sum.Lex.LT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }
theorem
Sum.Lex.inl_strictMono
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
:
StrictMono (⇑toLex ∘ inl)
theorem
Sum.Lex.inr_strictMono
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
:
StrictMono (⇑toLex ∘ inr)
instance
Sum.Lex.partialOrder
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[PartialOrder β]
:
PartialOrder (_root_.Lex (α ⊕ β))
Equations
- Sum.Lex.partialOrder = { toPreorder := Sum.Lex.preorder, le_antisymm := ⋯ }
instance
Sum.Lex.linearOrder
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[LinearOrder β]
:
LinearOrder (_root_.Lex (α ⊕ β))
Equations
- One or more equations did not get rendered due to their size.
instance
Sum.Lex.boundedOrder
{α : Type u_1}
{β : Type u_2}
[LE α]
[LE β]
[OrderBot α]
[OrderTop β]
:
BoundedOrder (_root_.Lex (α ⊕ β))
Equations
- Sum.Lex.boundedOrder = { toOrderTop := Sum.Lex.orderTop, toOrderBot := Sum.Lex.orderBot }
instance
Sum.Lex.noMinOrder
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[NoMinOrder α]
[NoMinOrder β]
:
NoMinOrder (_root_.Lex (α ⊕ β))
instance
Sum.Lex.noMaxOrder
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[NoMaxOrder α]
[NoMaxOrder β]
:
NoMaxOrder (_root_.Lex (α ⊕ β))
instance
Sum.Lex.noMinOrder_of_nonempty
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[NoMinOrder α]
[Nonempty α]
:
NoMinOrder (_root_.Lex (α ⊕ β))
instance
Sum.Lex.noMaxOrder_of_nonempty
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[NoMaxOrder β]
[Nonempty β]
:
NoMaxOrder (_root_.Lex (α ⊕ β))
instance
Sum.Lex.denselyOrdered_of_noMaxOrder
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[DenselyOrdered α]
[DenselyOrdered β]
[NoMaxOrder α]
:
DenselyOrdered (_root_.Lex (α ⊕ β))
instance
Sum.Lex.denselyOrdered_of_noMinOrder
{α : Type u_1}
{β : Type u_2}
[LT α]
[LT β]
[DenselyOrdered α]
[DenselyOrdered β]
[NoMinOrder β]
:
DenselyOrdered (_root_.Lex (α ⊕ β))
Order isomorphisms #
Equiv.sumComm
promoted to an order isomorphism.
Equations
- OrderIso.sumComm α β = { toEquiv := Equiv.sumComm α β, map_rel_iff' := ⋯ }
Instances For
Equiv.sumAssoc
promoted to an order isomorphism.
Equations
- OrderIso.sumAssoc α β γ = { toEquiv := Equiv.sumAssoc α β γ, map_rel_iff' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
OrderIso.sumLexDualAntidistrib_symm_inl
{α : Type u_1}
{β : Type u_2}
[LE α]
[LE β]
(b : β)
:
@[simp]
theorem
OrderIso.sumLexDualAntidistrib_symm_inr
{α : Type u_1}
{β : Type u_2}
[LE α]
[LE β]
(a : α)
:
WithBot α
is order-isomorphic to PUnit ⊕ₗ α
, by sending ⊥
to Unit
and ↑a
to
a
.
Equations
- WithBot.orderIsoPUnitSumLex = { toEquiv := (Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit.{?u.14 + 1}).trans toLex), map_rel_iff' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
WithTop α
is order-isomorphic to α ⊕ₗ PUnit
, by sending ⊤
to Unit
and ↑a
to
a
.
Equations
- WithTop.orderIsoSumLexPUnit = { toEquiv := (Equiv.optionEquivSumPUnit α).trans toLex, map_rel_iff' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]