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.instIsReflSumLiftRel
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsRefl α r]
[inst : IsRefl β s]
:
IsRefl (α ⊕ β) (Sum.LiftRel r s)
instance
Sum.instIsIrreflSumLiftRel
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsIrrefl α r]
[inst : IsIrrefl β s]
:
IsIrrefl (α ⊕ β) (Sum.LiftRel r s)
theorem
Sum.LiftRel.trans
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsTrans α r]
[inst : IsTrans β s]
{a : α ⊕ β}
{b : α ⊕ β}
{c : α ⊕ β}
:
Sum.LiftRel r s a b → Sum.LiftRel r s b c → Sum.LiftRel r s a c
instance
Sum.instIsTransSumLiftRel
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsTrans α r]
[inst : IsTrans β s]
:
IsTrans (α ⊕ β) (Sum.LiftRel r s)
instance
Sum.instIsAntisymmSumLiftRel
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsAntisymm α r]
[inst : IsAntisymm β s]
:
IsAntisymm (α ⊕ β) (Sum.LiftRel r s)
instance
Sum.instIsAntisymmSumLex
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsAntisymm α r]
[inst : IsAntisymm β s]
:
IsAntisymm (α ⊕ β) (Sum.Lex r s)
instance
Sum.instIsTrichotomousSumLex
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsTrichotomous α r]
[inst : IsTrichotomous β s]
:
IsTrichotomous (α ⊕ β) (Sum.Lex r s)
instance
Sum.instIsWellOrderSumLex
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
[inst : IsWellOrder α r]
[inst : IsWellOrder β s]
:
IsWellOrder (α ⊕ β) (Sum.Lex r s)
Disjoint sum of two orders #
theorem
Sum.inl_strictMono
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
:
StrictMono Sum.inl
theorem
Sum.inr_strictMono
{α : Type u_2}
{β : Type u_1}
[inst : Preorder α]
[inst : Preorder β]
:
StrictMono Sum.inr
instance
Sum.instPartialOrderSum
{α : Type u_1}
{β : Type u_2}
[inst : PartialOrder α]
[inst : PartialOrder β]
:
PartialOrder (α ⊕ β)
Equations
- Sum.instPartialOrderSum = let src := Sum.instPreorderSum; PartialOrder.mk (_ : ∀ (x x_1 : α ⊕ β), Sum.LiftRel (fun x x_2 => x ≤ x_2) (fun x x_2 => x ≤ x_2) x x_1 → x_1 ≤ x → x = x_1)
instance
Sum.noMinOrder
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : NoMinOrder α]
[inst : NoMinOrder β]
:
NoMinOrder (α ⊕ β)
Equations
instance
Sum.noMaxOrder
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : NoMaxOrder α]
[inst : NoMaxOrder β]
:
NoMaxOrder (α ⊕ β)
Equations
@[simp]
theorem
Sum.noMinOrder_iff
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
:
NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β
@[simp]
theorem
Sum.noMaxOrder_iff
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
:
NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β
instance
Sum.denselyOrdered
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : DenselyOrdered α]
[inst : DenselyOrdered β]
:
DenselyOrdered (α ⊕ β)
@[simp]
theorem
Sum.denselyOrdered_iff
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
:
DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β
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))
theorem
Sum.Lex.toLex_strictMono
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
:
StrictMono ↑toLex
theorem
Sum.Lex.inl_strictMono
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
:
StrictMono (↑toLex ∘ Sum.inl)
theorem
Sum.Lex.inr_strictMono
{α : Type u_2}
{β : Type u_1}
[inst : Preorder α]
[inst : Preorder β]
:
StrictMono (↑toLex ∘ Sum.inr)
instance
Sum.Lex.partialOrder
{α : Type u_1}
{β : Type u_2}
[inst : PartialOrder α]
[inst : PartialOrder β]
:
PartialOrder (Lex (α ⊕ β))
Equations
- One or more equations did not get rendered due to their size.
instance
Sum.Lex.linearOrder
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder α]
[inst : LinearOrder β]
:
LinearOrder (Lex (α ⊕ β))
Equations
- One or more equations did not get rendered due to their size.
instance
Sum.Lex.noMinOrder
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : NoMinOrder α]
[inst : NoMinOrder β]
:
NoMinOrder (Lex (α ⊕ β))
instance
Sum.Lex.noMaxOrder
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : NoMaxOrder α]
[inst : NoMaxOrder β]
:
NoMaxOrder (Lex (α ⊕ β))
instance
Sum.Lex.noMinOrder_of_nonempty
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : NoMinOrder α]
[inst : Nonempty α]
:
NoMinOrder (Lex (α ⊕ β))
instance
Sum.Lex.noMaxOrder_of_nonempty
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : NoMaxOrder β]
[inst : Nonempty β]
:
NoMaxOrder (Lex (α ⊕ β))
instance
Sum.Lex.denselyOrdered_of_noMaxOrder
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : DenselyOrdered α]
[inst : DenselyOrdered β]
[inst : NoMaxOrder α]
:
DenselyOrdered (Lex (α ⊕ β))
instance
Sum.Lex.denselyOrdered_of_noMinOrder
{α : Type u_1}
{β : Type u_2}
[inst : LT α]
[inst : LT β]
[inst : DenselyOrdered α]
[inst : DenselyOrdered β]
[inst : NoMinOrder β]
:
DenselyOrdered (Lex (α ⊕ β))
Order isomorphisms #
@[simp]
theorem
OrderIso.sumComm_apply
(α : Type u_1)
(β : Type u_2)
[inst : LE α]
[inst : LE β]
:
∀ (a : α ⊕ β), ↑(RelIso.toRelEmbedding (OrderIso.sumComm α β)).toEmbedding a = Sum.swap a
@[simp]
theorem
OrderIso.sumComm_symm
(α : Type u_1)
(β : Type u_2)
[inst : LE α]
[inst : LE β]
:
OrderIso.symm (OrderIso.sumComm α β) = OrderIso.sumComm β α
@[simp]
theorem
OrderIso.sumAssoc_apply_inl_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.sumAssoc α β γ)).toEmbedding (Sum.inl (Sum.inl a)) = Sum.inl a
@[simp]
theorem
OrderIso.sumAssoc_apply_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(c : γ)
:
↑(RelIso.toRelEmbedding (OrderIso.sumAssoc α β γ)).toEmbedding (Sum.inr c) = Sum.inr (Sum.inr c)
@[simp]
theorem
OrderIso.sumAssoc_symm_apply_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumAssoc α β γ))).toEmbedding (Sum.inl a) = Sum.inl (Sum.inl a)
@[simp]
theorem
OrderIso.sumAssoc_symm_apply_inr_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumAssoc α β γ))).toEmbedding (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
@[simp]
theorem
OrderIso.sumAssoc_symm_apply_inr_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(c : γ)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumAssoc α β γ))).toEmbedding (Sum.inr (Sum.inr c)) = Sum.inr c
@[simp]
theorem
OrderIso.sumDualDistrib_inl
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.sumDualDistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inl a)) = Sum.inl (↑OrderDual.toDual a)
@[simp]
theorem
OrderIso.sumDualDistrib_inr
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.sumDualDistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inr b)) = Sum.inr (↑OrderDual.toDual b)
@[simp]
theorem
OrderIso.sumDualDistrib_symm_inl
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumDualDistrib α β))).toEmbedding (Sum.inl (↑OrderDual.toDual a)) = ↑OrderDual.toDual (Sum.inl a)
@[simp]
theorem
OrderIso.sumDualDistrib_symm_inr
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumDualDistrib α β))).toEmbedding (Sum.inr (↑OrderDual.toDual b)) = ↑OrderDual.toDual (Sum.inr b)
@[simp]
theorem
OrderIso.sumLexAssoc_apply_inl_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.sumLexAssoc α β γ)).toEmbedding (↑toLex (Sum.inl (↑toLex (Sum.inl a)))) = ↑toLex (Sum.inl a)
@[simp]
theorem
OrderIso.sumLexAssoc_apply_inl_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.sumLexAssoc α β γ)).toEmbedding (↑toLex (Sum.inl (↑toLex (Sum.inr b)))) = ↑toLex (Sum.inr (↑toLex (Sum.inl b)))
@[simp]
theorem
OrderIso.sumLexAssoc_apply_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(c : γ)
:
↑(RelIso.toRelEmbedding (OrderIso.sumLexAssoc α β γ)).toEmbedding (↑toLex (Sum.inr c)) = ↑toLex (Sum.inr (↑toLex (Sum.inr c)))
@[simp]
theorem
OrderIso.sumLexAssoc_symm_apply_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexAssoc α β γ))).toEmbedding (Sum.inl a) = Sum.inl (Sum.inl a)
@[simp]
theorem
OrderIso.sumLexAssoc_symm_apply_inr_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexAssoc α β γ))).toEmbedding (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
@[simp]
theorem
OrderIso.sumLexAssoc_symm_apply_inr_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : LE α]
[inst : LE β]
[inst : LE γ]
(c : γ)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexAssoc α β γ))).toEmbedding (Sum.inr (Sum.inr c)) = Sum.inr c
@[simp]
theorem
OrderIso.sumLexDualAntidistrib_inl
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.sumLexDualAntidistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inl a)) = Sum.inr (↑OrderDual.toDual a)
@[simp]
theorem
OrderIso.sumLexDualAntidistrib_inr
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.sumLexDualAntidistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inr b)) = Sum.inl (↑OrderDual.toDual b)
@[simp]
theorem
OrderIso.sumLexDualAntidistrib_symm_inl
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(b : β)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexDualAntidistrib α β))).toEmbedding
(Sum.inl (↑OrderDual.toDual b)) = ↑OrderDual.toDual (Sum.inr b)
@[simp]
theorem
OrderIso.sumLexDualAntidistrib_symm_inr
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexDualAntidistrib α β))).toEmbedding
(Sum.inr (↑OrderDual.toDual a)) = ↑OrderDual.toDual (Sum.inl a)
@[simp]
theorem
WithBot.orderIsoPUnitSumLex_bot
{α : Type u_1}
[inst : LE α]
:
↑(RelIso.toRelEmbedding WithBot.orderIsoPUnitSumLex).toEmbedding ⊥ = ↑toLex (Sum.inl PUnit.unit)
@[simp]
theorem
WithBot.orderIsoPUnitSumLex_toLex
{α : Type u_1}
[inst : LE α]
(a : α)
:
↑(RelIso.toRelEmbedding WithBot.orderIsoPUnitSumLex).toEmbedding ↑a = ↑toLex (Sum.inr a)
@[simp]
theorem
WithBot.orderIsoPUnitSumLex_symm_inl
{α : Type u_2}
[inst : LE α]
(x : PUnit)
:
↑(RelIso.toRelEmbedding (OrderIso.symm WithBot.orderIsoPUnitSumLex)).toEmbedding (↑toLex (Sum.inl x)) = ⊥
@[simp]
theorem
WithBot.orderIsoPUnitSumLex_symm_inr
{α : Type u_1}
[inst : LE α]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.symm WithBot.orderIsoPUnitSumLex)).toEmbedding (↑toLex (Sum.inr a)) = ↑a
@[simp]
theorem
WithTop.orderIsoSumLexPUnit_top
{α : Type u_1}
[inst : LE α]
:
↑(RelIso.toRelEmbedding WithTop.orderIsoSumLexPUnit).toEmbedding ⊤ = ↑toLex (Sum.inr PUnit.unit)
@[simp]
theorem
WithTop.orderIsoSumLexPUnit_toLex
{α : Type u_1}
[inst : LE α]
(a : α)
:
↑(RelIso.toRelEmbedding WithTop.orderIsoSumLexPUnit).toEmbedding ↑a = ↑toLex (Sum.inl a)
@[simp]
theorem
WithTop.orderIsoSumLexPUnit_symm_inr
{α : Type u_2}
[inst : LE α]
(x : PUnit)
:
↑(RelIso.toRelEmbedding (OrderIso.symm WithTop.orderIsoSumLexPUnit)).toEmbedding (↑toLex (Sum.inr x)) = ⊤
@[simp]
theorem
WithTop.orderIsoSumLexPUnit_symm_inl
{α : Type u_1}
[inst : LE α]
(a : α)
:
↑(RelIso.toRelEmbedding (OrderIso.symm WithTop.orderIsoSumLexPUnit)).toEmbedding (↑toLex (Sum.inl a)) = ↑a