data.sum.order - mathlib3 docs

@[refl]

theorem sum.lift_rel.refl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_refl α r] [is_refl β s] (x : α ⊕ β) :

sum.lift_rel r s x x

source

@[protected, instance]

def sum.lift_rel.is_refl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_refl α r] [is_refl β s] :

is_refl (α ⊕ β) (sum.lift_rel r s)

source

@[protected, instance]

def sum.lift_rel.is_irrefl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_irrefl α r] [is_irrefl β s] :

is_irrefl (α ⊕ β) (sum.lift_rel r s)

source

@[trans]

theorem sum.lift_rel.trans {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_trans α r] [is_trans β s] {a b c : α ⊕ β} :

sum.lift_rel r s a b → sum.lift_rel r s b c → sum.lift_rel r s a c

source

@[protected, instance]

def sum.lift_rel.is_trans {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_trans α r] [is_trans β s] :

is_trans (α ⊕ β) (sum.lift_rel r s)

source

@[protected, instance]

def sum.lift_rel.is_antisymm {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_antisymm α r] [is_antisymm β s] :

is_antisymm (α ⊕ β) (sum.lift_rel r s)

source

@[protected, instance]

def sum.lex.is_refl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_refl α r] [is_refl β s] :

is_refl (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.lex.is_irrefl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_irrefl α r] [is_irrefl β s] :

is_irrefl (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.lex.is_trans {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_trans α r] [is_trans β s] :

is_trans (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.lex.is_antisymm {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_antisymm α r] [is_antisymm β s] :

is_antisymm (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.lex.is_total {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_total α r] [is_total β s] :

is_total (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.lex.is_trichotomous {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_trichotomous α r] [is_trichotomous β s] :

is_trichotomous (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.lex.is_well_order {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_well_order α r] [is_well_order β s] :

is_well_order (α ⊕ β) (sum.lex r s)

source

@[protected, instance]

def sum.has_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :

has_le (α ⊕ β)

Equations

sum.has_le = {le := sum.lift_rel has_le.le has_le.le}

source

@[protected, instance]

def sum.has_lt {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :

has_lt (α ⊕ β)

Equations

sum.has_lt = {lt := sum.lift_rel has_lt.lt has_lt.lt}

source

theorem sum.le_def {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α ⊕ β} :

a ≤ b ↔ sum.lift_rel has_le.le has_le.le a b

source

theorem sum.lt_def {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α ⊕ β} :

a < b ↔ sum.lift_rel has_lt.lt has_lt.lt a b

source

@[simp]

theorem sum.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α} :

sum.inl a ≤ sum.inl b ↔ a ≤ b

source

@[simp]

theorem sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : β} :

sum.inr a ≤ sum.inr b ↔ a ≤ b

source

@[simp]

theorem sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α} :

sum.inl a < sum.inl b ↔ a < b

source

@[simp]

theorem sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : β} :

sum.inr a < sum.inr b ↔ a < b

source

@[simp]

theorem sum.not_inl_le_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a : α} {b : β} :

¬sum.inl b ≤ sum.inr a

source

@[simp]

theorem sum.not_inl_lt_inr {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a : α} {b : β} :

¬sum.inl b < sum.inr a

source

@[simp]

theorem sum.not_inr_le_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a : α} {b : β} :

¬sum.inr b ≤ sum.inl a

source

@[simp]

theorem sum.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a : α} {b : β} :

¬sum.inr b < sum.inl a

source

@[protected, instance]

def sum.preorder {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

preorder (α ⊕ β)

Equations

sum.preorder = {le := has_le.le sum.has_le, lt := has_lt.lt sum.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

theorem sum.inl_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

monotone sum.inl

source

theorem sum.inr_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

monotone sum.inr

source

theorem sum.inl_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

strict_mono sum.inl

source

theorem sum.inr_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

strict_mono sum.inr

source

@[protected, instance]

def sum.partial_order {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] :

partial_order (α ⊕ β)

Equations

sum.partial_order = {le := preorder.le sum.preorder, lt := preorder.lt sum.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def sum.no_min_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_min_order α] [no_min_order β] :

no_min_order (α ⊕ β)

source

@[protected, instance]

def sum.no_max_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_max_order α] [no_max_order β] :

no_max_order (α ⊕ β)

source

@[simp]

theorem sum.no_min_order_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :

no_min_order (α ⊕ β) ↔ no_min_order α ∧ no_min_order β

source

@[simp]

theorem sum.no_max_order_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :

no_max_order (α ⊕ β) ↔ no_max_order α ∧ no_max_order β

source

@[protected, instance]

def sum.densely_ordered {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [densely_ordered α] [densely_ordered β] :

densely_ordered (α ⊕ β)

source

@[simp]

theorem sum.densely_ordered_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :

densely_ordered (α ⊕ β) ↔ densely_ordered α ∧ densely_ordered β

source

@[simp]

theorem sum.swap_le_swap_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α ⊕ β} :

a.swap ≤ b.swap ↔ a ≤ b

source

@[simp]

theorem sum.swap_lt_swap_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α ⊕ β} :

a.swap < b.swap ↔ a < b

source

@[reducible]

def sum.inlₗ {α : Type u_1} {β : Type u_2} (x : α) :

α ⊕ₗ β

Lexicographical sum.inl. Only used for pattern matching.

source

@[reducible]

def sum.inrₗ {α : Type u_1} {β : Type u_2} (x : β) :

α ⊕ₗ β

Lexicographical sum.inr. Only used for pattern matching.

source

@[protected, instance]

def sum.lex.has_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :

has_le (α ⊕ₗ β)

The linear/lexicographical ≤ on a sum.

Equations

sum.lex.has_le = {le := sum.lex has_le.le has_le.le}

source

@[protected, instance]

def sum.lex.has_lt {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :

has_lt (α ⊕ₗ β)

The linear/lexicographical < on a sum.

Equations

sum.lex.has_lt = {lt := sum.lex has_lt.lt has_lt.lt}

source

@[simp]

theorem sum.lex.to_lex_le_to_lex {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α ⊕ β} :

⇑to_lex a ≤ ⇑to_lex b ↔ sum.lex has_le.le has_le.le a b

source

@[simp]

theorem sum.lex.to_lex_lt_to_lex {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α ⊕ β} :

⇑to_lex a < ⇑to_lex b ↔ sum.lex has_lt.lt has_lt.lt a b

source

theorem sum.lex.le_def {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α ⊕ₗ β} :

a ≤ b ↔ sum.lex has_le.le has_le.le (⇑of_lex a) (⇑of_lex b)

source

theorem sum.lex.lt_def {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α ⊕ₗ β} :

a < b ↔ sum.lex has_lt.lt has_lt.lt (⇑of_lex a) (⇑of_lex b)

source

@[simp]

theorem sum.lex.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α} :

⇑to_lex (sum.inl a) ≤ ⇑to_lex (sum.inl b) ↔ a ≤ b

source

@[simp]

theorem sum.lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : β} :

⇑to_lex (sum.inr a) ≤ ⇑to_lex (sum.inr b) ↔ a ≤ b

source

@[simp]

theorem sum.lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α} :

⇑to_lex (sum.inl a) < ⇑to_lex (sum.inl b) ↔ a < b

source

@[simp]

theorem sum.lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : β} :

⇑to_lex (sum.inr a) < ⇑to_lex (sum.inr b) ↔ a < b

source

@[simp]

theorem sum.lex.inl_le_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) (b : β) :

⇑to_lex (sum.inl a) ≤ ⇑to_lex (sum.inr b)

source

@[simp]

theorem sum.lex.inl_lt_inr {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (a : α) (b : β) :

⇑to_lex (sum.inl a) < ⇑to_lex (sum.inr b)

source

@[simp]

theorem sum.lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a : α} {b : β} :

¬⇑to_lex (sum.inr b) ≤ ⇑to_lex (sum.inl a)

source

@[simp]

theorem sum.lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a : α} {b : β} :

¬⇑to_lex (sum.inr b) < ⇑to_lex (sum.inl a)

source

@[protected, instance]

def sum.lex.preorder {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

preorder (α ⊕ₗ β)

Equations

sum.lex.preorder = {le := has_le.le sum.lex.has_le, lt := has_lt.lt sum.lex.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

theorem sum.lex.to_lex_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

monotone ⇑to_lex

source

theorem sum.lex.to_lex_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

strict_mono ⇑to_lex

source

theorem sum.lex.inl_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

monotone (⇑to_lex ∘ sum.inl)

source

theorem sum.lex.inr_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

monotone (⇑to_lex ∘ sum.inr)

source

theorem sum.lex.inl_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

strict_mono (⇑to_lex ∘ sum.inl)

source

theorem sum.lex.inr_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

strict_mono (⇑to_lex ∘ sum.inr)

source

@[protected, instance]

def sum.lex.partial_order {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] :

partial_order (α ⊕ₗ β)

Equations

sum.lex.partial_order = {le := preorder.le sum.lex.preorder, lt := preorder.lt sum.lex.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def sum.lex.linear_order {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] :

linear_order (α ⊕ₗ β)

Equations

sum.lex.linear_order = {le := partial_order.le sum.lex.partial_order, lt := partial_order.lt sum.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := sum.lex.decidable_rel (λ (a b : β), has_le.le.decidable a b), decidable_eq := sum.decidable_eq α β (λ (a b : β), eq.decidable a b), decidable_lt := decidable_lt_of_decidable_le sum.lex.decidable_rel, max := max_default (λ (a b : α ⊕ₗ β), sum.lex.decidable_rel a b), max_def := _, min := min_default (λ (a b : α ⊕ₗ β), sum.lex.decidable_rel a b), min_def := _}

source

@[protected, instance]

def sum.lex.order_bot {α : Type u_1} {β : Type u_2} [has_le α] [order_bot α] [has_le β] :

order_bot (α ⊕ₗ β)

The lexicographical bottom of a sum is the bottom of the left component.

Equations

sum.lex.order_bot = {bot := sum.inl ⊥, bot_le := _}

source

@[simp]

theorem sum.lex.inl_bot {α : Type u_1} {β : Type u_2} [has_le α] [order_bot α] [has_le β] :

⇑to_lex (sum.inl ⊥) = ⊥

source

@[protected, instance]

def sum.lex.order_top {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] [order_top β] :

order_top (α ⊕ₗ β)

The lexicographical top of a sum is the top of the right component.

Equations

sum.lex.order_top = {top := sum.inr ⊤, le_top := _}

source

@[simp]

theorem sum.lex.inr_top {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] [order_top β] :

⇑to_lex (sum.inr ⊤) = ⊤

source

@[protected, instance]

def sum.lex.bounded_order {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] [order_bot α] [order_top β] :

bounded_order (α ⊕ₗ β)

Equations

sum.lex.bounded_order = {top := order_top.top sum.lex.order_top, le_top := _, bot := order_bot.bot sum.lex.order_bot, bot_le := _}

source

@[protected, instance]

def sum.lex.no_min_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_min_order α] [no_min_order β] :

no_min_order (α ⊕ₗ β)

source

@[protected, instance]

def sum.lex.no_max_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_max_order α] [no_max_order β] :

no_max_order (α ⊕ₗ β)

source

@[protected, instance]

def sum.lex.no_min_order_of_nonempty {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_min_order α] [nonempty α] :

no_min_order (α ⊕ₗ β)

source

@[protected, instance]

def sum.lex.no_max_order_of_nonempty {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_max_order β] [nonempty β] :

no_max_order (α ⊕ₗ β)

source

@[protected, instance]

def sum.lex.densely_ordered_of_no_max_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [densely_ordered α] [densely_ordered β] [no_max_order α] :

densely_ordered (α ⊕ₗ β)

source

@[protected, instance]

def sum.lex.densely_ordered_of_no_min_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [densely_ordered α] [densely_ordered β] [no_min_order β] :

densely_ordered (α ⊕ₗ β)

source

def order_iso.sum_comm (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :

α ⊕ β ≃o β ⊕ α

equiv.sum_comm promoted to an order isomorphism.

Equations

order_iso.sum_comm α β = {to_equiv := {to_fun := (equiv.sum_comm α β).to_fun, inv_fun := (equiv.sum_comm α β).inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.sum_comm_apply (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] (ᾰ : α ⊕ β) :

⇑(order_iso.sum_comm α β) ᾰ = (equiv.sum_comm α β).to_fun ᾰ

source

@[simp]

theorem order_iso.sum_comm_symm (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :

(order_iso.sum_comm α β).symm = order_iso.sum_comm β α

source

def order_iso.sum_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [has_le α] [has_le β] [has_le γ] :

(α ⊕ β) ⊕ γ ≃o α ⊕ β ⊕ γ

equiv.sum_assoc promoted to an order isomorphism.

Equations

order_iso.sum_assoc α β γ = {to_equiv := {to_fun := (equiv.sum_assoc α β γ).to_fun, inv_fun := (equiv.sum_assoc α β γ).inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.sum_assoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :

⇑(order_iso.sum_assoc α β γ) (sum.inl (sum.inl a)) = sum.inl a

source

@[simp]

theorem order_iso.sum_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :

⇑(order_iso.sum_assoc α β γ) (sum.inl (sum.inr b)) = sum.inr (sum.inl b)

source

@[simp]

theorem order_iso.sum_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :

⇑(order_iso.sum_assoc α β γ) (sum.inr c) = sum.inr (sum.inr c)

source

@[simp]

theorem order_iso.sum_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :

⇑((order_iso.sum_assoc α β γ).symm) (sum.inl a) = sum.inl (sum.inl a)

source

@[simp]

theorem order_iso.sum_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :

⇑((order_iso.sum_assoc α β γ).symm) (sum.inr (sum.inl b)) = sum.inl (sum.inr b)

source

@[simp]

theorem order_iso.sum_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :

⇑((order_iso.sum_assoc α β γ).symm) (sum.inr (sum.inr c)) = sum.inr c

source

def order_iso.sum_dual_distrib (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :

(α ⊕ β)ᵒᵈ ≃o αᵒᵈ ⊕ βᵒᵈ

order_dual is distributive over ⊕ up to an order isomorphism.

Equations

order_iso.sum_dual_distrib α β = {to_equiv := {to_fun := (equiv.refl (α ⊕ β)ᵒᵈ).to_fun, inv_fun := (equiv.refl (α ⊕ β)ᵒᵈ).inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.sum_dual_distrib_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :

⇑(order_iso.sum_dual_distrib α β) (⇑order_dual.to_dual (sum.inl a)) = sum.inl (⇑order_dual.to_dual a)

source

@[simp]

theorem order_iso.sum_dual_distrib_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :

⇑(order_iso.sum_dual_distrib α β) (⇑order_dual.to_dual (sum.inr b)) = sum.inr (⇑order_dual.to_dual b)

source

@[simp]

theorem order_iso.sum_dual_distrib_symm_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :

⇑((order_iso.sum_dual_distrib α β).symm) (sum.inl (⇑order_dual.to_dual a)) = ⇑order_dual.to_dual (sum.inl a)

source

@[simp]

theorem order_iso.sum_dual_distrib_symm_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :

⇑((order_iso.sum_dual_distrib α β).symm) (sum.inr (⇑order_dual.to_dual b)) = ⇑order_dual.to_dual (sum.inr b)

source

def order_iso.sum_lex_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [has_le α] [has_le β] [has_le γ] :

(α ⊕ₗ β) ⊕ₗ γ ≃o α ⊕ₗ β ⊕ₗ γ

equiv.sum_assoc promoted to an order isomorphism.

Equations

order_iso.sum_lex_assoc α β γ = {to_equiv := {to_fun := (equiv.sum_assoc α β γ).to_fun, inv_fun := (equiv.sum_assoc α β γ).inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.sum_lex_assoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :

⇑(order_iso.sum_lex_assoc α β γ) (⇑to_lex (sum.inl (⇑to_lex (sum.inl a)))) = ⇑to_lex (sum.inl a)

source

@[simp]

theorem order_iso.sum_lex_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :

⇑(order_iso.sum_lex_assoc α β γ) (⇑to_lex (sum.inl (⇑to_lex (sum.inr b)))) = ⇑to_lex (sum.inr (⇑to_lex (sum.inl b)))

source

@[simp]

theorem order_iso.sum_lex_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :

⇑(order_iso.sum_lex_assoc α β γ) (⇑to_lex (sum.inr c)) = ⇑to_lex (sum.inr (⇑to_lex (sum.inr c)))

source

@[simp]

theorem order_iso.sum_lex_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :

⇑((order_iso.sum_lex_assoc α β γ).symm) (sum.inl a) = sum.inl (sum.inl a)

source

@[simp]

theorem order_iso.sum_lex_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :

⇑((order_iso.sum_lex_assoc α β γ).symm) (sum.inr (sum.inl b)) = sum.inl (sum.inr b)

source

@[simp]

theorem order_iso.sum_lex_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :

⇑((order_iso.sum_lex_assoc α β γ).symm) (sum.inr (sum.inr c)) = sum.inr c

source

def order_iso.sum_lex_dual_antidistrib (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :

(α ⊕ₗ β)ᵒᵈ ≃o βᵒᵈ ⊕ₗ αᵒᵈ

order_dual is antidistributive over ⊕ₗ up to an order isomorphism.

Equations

order_iso.sum_lex_dual_antidistrib α β = {to_equiv := {to_fun := (equiv.sum_comm α β).to_fun, inv_fun := (equiv.sum_comm α β).inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.sum_lex_dual_antidistrib_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :

⇑(order_iso.sum_lex_dual_antidistrib α β) (⇑order_dual.to_dual (sum.inl a)) = sum.inr (⇑order_dual.to_dual a)

source

@[simp]

theorem order_iso.sum_lex_dual_antidistrib_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :

⇑(order_iso.sum_lex_dual_antidistrib α β) (⇑order_dual.to_dual (sum.inr b)) = sum.inl (⇑order_dual.to_dual b)

source

@[simp]

theorem order_iso.sum_lex_dual_antidistrib_symm_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :

⇑((order_iso.sum_lex_dual_antidistrib α β).symm) (sum.inl (⇑order_dual.to_dual b)) = ⇑order_dual.to_dual (sum.inr b)

source

@[simp]

theorem order_iso.sum_lex_dual_antidistrib_symm_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :

⇑((order_iso.sum_lex_dual_antidistrib α β).symm) (sum.inr (⇑order_dual.to_dual a)) = ⇑order_dual.to_dual (sum.inl a)

source

def with_bot.order_iso_punit_sum_lex {α : Type u_1} [has_le α] :

with_bot α ≃o punit ⊕ₗ α

with_bot α is order-isomorphic to punit ⊕ₗ α, by sending ⊥ to punit.star and ↑a to a.

Equations

with_bot.order_iso_punit_sum_lex = {to_equiv := (equiv.option_equiv_sum_punit α).trans ((equiv.sum_comm α punit).trans to_lex), map_rel_iff' := _}

source

@[simp]

theorem with_bot.order_iso_punit_sum_lex_bot {α : Type u_1} [has_le α] :

⇑with_bot.order_iso_punit_sum_lex ⊥ = ⇑to_lex (sum.inl punit.star)

source

@[simp]

theorem with_bot.order_iso_punit_sum_lex_coe {α : Type u_1} [has_le α] (a : α) :

⇑with_bot.order_iso_punit_sum_lex ↑a = ⇑to_lex (sum.inr a)

source

@[simp]

theorem with_bot.order_iso_punit_sum_lex_symm_inl {α : Type u_1} [has_le α] (x : punit) :

⇑(with_bot.order_iso_punit_sum_lex.symm) (⇑to_lex (sum.inl x)) = ⊥

source

@[simp]

theorem with_bot.order_iso_punit_sum_lex_symm_inr {α : Type u_1} [has_le α] (a : α) :

⇑(with_bot.order_iso_punit_sum_lex.symm) (⇑to_lex (sum.inr a)) = ↑a

source

def with_top.order_iso_sum_lex_punit {α : Type u_1} [has_le α] :

with_top α ≃o α ⊕ₗ punit

with_top α is order-isomorphic to α ⊕ₗ punit, by sending ⊤ to punit.star and ↑a to a.

Equations

with_top.order_iso_sum_lex_punit = {to_equiv := (equiv.option_equiv_sum_punit α).trans to_lex, map_rel_iff' := _}

source

@[simp]

theorem with_top.order_iso_sum_lex_punit_top {α : Type u_1} [has_le α] :

⇑with_top.order_iso_sum_lex_punit ⊤ = ⇑to_lex (sum.inr punit.star)

source

@[simp]

theorem with_top.order_iso_sum_lex_punit_coe {α : Type u_1} [has_le α] (a : α) :

⇑with_top.order_iso_sum_lex_punit ↑a = ⇑to_lex (sum.inl a)

source

@[simp]

theorem with_top.order_iso_sum_lex_punit_symm_inr {α : Type u_1} [has_le α] (x : punit) :

⇑(with_top.order_iso_sum_lex_punit.symm) (⇑to_lex (sum.inr x)) = ⊤

source

@[simp]

theorem with_top.order_iso_sum_lex_punit_symm_inl {α : Type u_1} [has_le α] (a : α) :

⇑(with_top.order_iso_sum_lex_punit.symm) (⇑to_lex (sum.inl a)) = ↑a

mathlib3 documentation

Orders on a sum type #

Main declarations #

Notation #

Unbundled relation classes #

Disjoint sum of two orders #

Linear sum of two orders #

Order isomorphisms #