mathlib documentation

data.sum.order

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.lift_rel 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 #

Notation #

Unbundled relation classes #

source
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
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)

Disjoint sum of two orders #

source
@[protected, instance]
def sum.has_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :
has_le (α ⊕ β)
Equations
source
@[protected, instance]
def sum.has_lt {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :
has_lt (α ⊕ β)
Equations
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
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
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

Linear sum of two orders #

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

Lexicographical sum.inl. Only used for pattern matching.

source
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
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
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
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
source
@[protected, instance]
def sum.lex.linear_order {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] :
linear_order (α ⊕ₗ β)
Equations
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
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
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
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 (α ⊕ₗ β)

Order isomorphisms #

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
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
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 β] :
order_dual (α ⊕ β) ≃o order_dual α ⊕ order_dual β

order_dual is distributive over ⊕ up to an order isomorphism.

Equations
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
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 β] :
order_dual (α ⊕ₗ β) ≃o order_dual β ⊕ₗ order_dual α

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

Equations
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)