Finite intervals in a disjoint union #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides the locally_finite_order instance for the disjoint sum and linear sum of two
orders and calculates the cardinality of their finite intervals.
@[simp]
def
finset.sum_lift₂
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
(f : α₁ → β₁ → finset γ₁)
(g : α₂ → β₂ → finset γ₂)
(a : α₁ ⊕ α₂)
(b : β₁ ⊕ β₂) :
Lifts maps α₁ → β₁ → finset γ₁ and α₂ → β₂ → finset γ₂ to a map
α₁ ⊕ α₂ → β₁ ⊕ β₂ → finset (γ₁ ⊕ γ₂). Could be generalized to alternative functors if we can
make sure to keep computability and universe polymorphism.
Equations
- finset.sum_lift₂ f g (sum.inr a) (sum.inr b) = finset.map function.embedding.inr (g a b)
- finset.sum_lift₂ f g (sum.inr a) (sum.inl b) = ∅
- finset.sum_lift₂ f g (sum.inl a) (sum.inr b) = ∅
- finset.sum_lift₂ f g (sum.inl a) (sum.inl b) = finset.map function.embedding.inl (f a b)
theorem
finset.sum_lift₂_mono
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
{f₁ g₁ : α₁ → β₁ → finset γ₁}
{f₂ g₂ : α₂ → β₂ → finset γ₂}
(h₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ g₁ a b)
(h₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ g₂ a b)
(a : α₁ ⊕ α₂)
(b : β₁ ⊕ β₂) :
finset.sum_lift₂ f₁ f₂ a b ⊆ finset.sum_lift₂ g₁ g₂ a b
def
finset.sum_lex_lift
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
(f₁ : α₁ → β₁ → finset γ₁)
(f₂ : α₂ → β₂ → finset γ₂)
(g₁ : α₁ → β₂ → finset γ₁)
(g₂ : α₁ → β₂ → finset γ₂)
(a : α₁ ⊕ α₂)
(b : β₁ ⊕ β₂) :
Lifts maps α₁ → β₁ → finset γ₁, α₂ → β₂ → finset γ₂, α₁ → β₂ → finset γ₁,
α₂ → β₂ → finset γ₂ to a map α₁ ⊕ α₂ → β₁ ⊕ β₂ → finset (γ₁ ⊕ γ₂). Could be generalized to
alternative monads if we can make sure to keep computability and universe polymorphism.
Equations
- finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inr a) (sum.inr b) = finset.map {to_fun := sum.inr γ₂, inj' := _} (f₂ a b)
- finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inr a) (sum.inl b) = ∅
- finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inl a) (sum.inr b) = (g₁ a b).disj_sum (g₂ a b)
- finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inl a) (sum.inl b) = finset.map function.embedding.inl (f₁ a b)
@[simp]
theorem
finset.sum_lex_lift_inl_inl
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
(f₁ : α₁ → β₁ → finset γ₁)
(f₂ : α₂ → β₂ → finset γ₂)
(g₁ : α₁ → β₂ → finset γ₁)
(g₂ : α₁ → β₂ → finset γ₂)
(a : α₁)
(b : β₁) :
finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inl a) (sum.inl b) = finset.map function.embedding.inl (f₁ a b)
@[simp]
theorem
finset.sum_lex_lift_inl_inr
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
(f₁ : α₁ → β₁ → finset γ₁)
(f₂ : α₂ → β₂ → finset γ₂)
(g₁ : α₁ → β₂ → finset γ₁)
(g₂ : α₁ → β₂ → finset γ₂)
(a : α₁)
(b : β₂) :
finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inl a) (sum.inr b) = (g₁ a b).disj_sum (g₂ a b)
@[simp]
theorem
finset.sum_lex_lift_inr_inl
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
(f₁ : α₁ → β₁ → finset γ₁)
(f₂ : α₂ → β₂ → finset γ₂)
(g₁ : α₁ → β₂ → finset γ₁)
(g₂ : α₁ → β₂ → finset γ₂)
(a : α₂)
(b : β₁) :
finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inr a) (sum.inl b) = ∅
@[simp]
theorem
finset.sum_lex_lift_inr_inr
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
(f₁ : α₁ → β₁ → finset γ₁)
(f₂ : α₂ → β₂ → finset γ₂)
(g₁ : α₁ → β₂ → finset γ₁)
(g₂ : α₁ → β₂ → finset γ₂)
(a : α₂)
(b : β₂) :
finset.sum_lex_lift f₁ f₂ g₁ g₂ (sum.inr a) (sum.inr b) = finset.map {to_fun := sum.inr γ₂, inj' := _} (f₂ a b)
theorem
finset.mem_sum_lex_lift
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
{f₁ : α₁ → β₁ → finset γ₁}
{f₂ : α₂ → β₂ → finset γ₂}
{g₁ : α₁ → β₂ → finset γ₁}
{g₂ : α₁ → β₂ → finset γ₂}
{a : α₁ ⊕ α₂}
{b : β₁ ⊕ β₂}
{c : γ₁ ⊕ γ₂} :
c ∈ finset.sum_lex_lift f₁ f₂ g₁ g₂ a b ↔ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = sum.inl a₁ ∧ b = sum.inl b₁ ∧ c = sum.inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁), a = sum.inl a₁ ∧ b = sum.inr b₂ ∧ c = sum.inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨ (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), a = sum.inl a₁ ∧ b = sum.inr b₂ ∧ c = sum.inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = sum.inr a₂ ∧ b = sum.inr b₂ ∧ c = sum.inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
theorem
finset.sum_lex_lift_mono
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
{f₁ f₁' : α₁ → β₁ → finset γ₁}
{f₂ f₂' : α₂ → β₂ → finset γ₂}
{g₁ g₁' : α₁ → β₂ → finset γ₁}
{g₂ g₂' : α₁ → β₂ → finset γ₂}
(hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b)
(hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b)
(hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b)
(hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b)
(a : α₁ ⊕ α₂)
(b : β₁ ⊕ β₂) :
finset.sum_lex_lift f₁ f₂ g₁ g₂ a b ⊆ finset.sum_lex_lift f₁' f₂' g₁' g₂' a b
theorem
finset.sum_lex_lift_nonempty
{α₁ : Type u_1}
{α₂ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{γ₁ : Type u_5}
{γ₂ : Type u_6}
{f₁ : α₁ → β₁ → finset γ₁}
{f₂ : α₂ → β₂ → finset γ₂}
{g₁ : α₁ → β₂ → finset γ₁}
{g₂ : α₁ → β₂ → finset γ₂}
{a : α₁ ⊕ α₂}
{b : β₁ ⊕ β₂} :
(finset.sum_lex_lift f₁ f₂ g₁ g₂ a b).nonempty ↔ (∃ (a₁ : α₁) (b₁ : β₁), a = sum.inl a₁ ∧ b = sum.inl b₁ ∧ (f₁ a₁ b₁).nonempty) ∨ (∃ (a₁ : α₁) (b₂ : β₂), a = sum.inl a₁ ∧ b = sum.inr b₂ ∧ ((g₁ a₁ b₂).nonempty ∨ (g₂ a₁ b₂).nonempty)) ∨ ∃ (a₂ : α₂) (b₂ : β₂), a = sum.inr a₂ ∧ b = sum.inr b₂ ∧ (f₂ a₂ b₂).nonempty
Disjoint sum of orders #
@[protected, instance]
def
sum.locally_finite_order
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β] :
locally_finite_order (α ⊕ β)
Equations
- sum.locally_finite_order = {finset_Icc := finset.sum_lift₂ finset.Icc finset.Icc, finset_Ico := finset.sum_lift₂ finset.Ico finset.Ico, finset_Ioc := finset.sum_lift₂ finset.Ioc finset.Ioc, finset_Ioo := finset.sum_lift₂ finset.Ioo finset.Ioo, finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
theorem
sum.Icc_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Icc (sum.inl a₁) (sum.inl a₂) = finset.map function.embedding.inl (finset.Icc a₁ a₂)
theorem
sum.Ico_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Ico (sum.inl a₁) (sum.inl a₂) = finset.map function.embedding.inl (finset.Ico a₁ a₂)
theorem
sum.Ioc_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Ioc (sum.inl a₁) (sum.inl a₂) = finset.map function.embedding.inl (finset.Ioc a₁ a₂)
theorem
sum.Ioo_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Ioo (sum.inl a₁) (sum.inl a₂) = finset.map function.embedding.inl (finset.Ioo a₁ a₂)
@[simp]
theorem
sum.Icc_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Icc (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Ico (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Ioc (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Ioo (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Icc (sum.inr b₁) (sum.inl a₂) = ∅
@[simp]
theorem
sum.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Ico (sum.inr b₁) (sum.inl a₂) = ∅
@[simp]
theorem
sum.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Ioc (sum.inr b₁) (sum.inl a₂) = ∅
@[simp]
theorem
sum.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Ioo (sum.inr b₁) (sum.inl a₂) = ∅
theorem
sum.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Icc (sum.inr b₁) (sum.inr b₂) = finset.map function.embedding.inr (finset.Icc b₁ b₂)
theorem
sum.Ico_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ico (sum.inr b₁) (sum.inr b₂) = finset.map function.embedding.inr (finset.Ico b₁ b₂)
theorem
sum.Ioc_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ioc (sum.inr b₁) (sum.inr b₂) = finset.map function.embedding.inr (finset.Ioc b₁ b₂)
theorem
sum.Ioo_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ioo (sum.inr b₁) (sum.inr b₂) = finset.map function.embedding.inr (finset.Ioo b₁ b₂)
Lexicographical sum of orders #
@[protected, instance]
def
sum.lex.locally_finite_order
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β] :
locally_finite_order (α ⊕ₗ β)
Equations
- sum.lex.locally_finite_order = {finset_Icc := λ (a b : α ⊕ₗ β), finset.map to_lex.to_embedding (finset.sum_lex_lift finset.Icc finset.Icc (λ (a : α) (_x : β), finset.Ici a) (λ (_x : α), finset.Iic) (⇑of_lex a) (⇑of_lex b)), finset_Ico := λ (a b : α ⊕ₗ β), finset.map to_lex.to_embedding (finset.sum_lex_lift finset.Ico finset.Ico (λ (a : α) (_x : β), finset.Ici a) (λ (_x : α), finset.Iio) (⇑of_lex a) (⇑of_lex b)), finset_Ioc := λ (a b : α ⊕ₗ β), finset.map to_lex.to_embedding (finset.sum_lex_lift finset.Ioc finset.Ioc (λ (a : α) (_x : β), finset.Ioi a) (λ (_x : α), finset.Iic) (⇑of_lex a) (⇑of_lex b)), finset_Ioo := λ (a b : α ⊕ₗ β), finset.map to_lex.to_embedding (finset.sum_lex_lift finset.Ioo finset.Ioo (λ (a : α) (_x : β), finset.Ioi a) (λ (_x : α), finset.Iio) (⇑of_lex a) (⇑of_lex b)), finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
theorem
sum.lex.Icc_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Icc (sum.inlₗ a₁) (sum.inlₗ a₂) = finset.map (function.embedding.inl.trans to_lex.to_embedding) (finset.Icc a₁ a₂)
theorem
sum.lex.Ico_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Ico (sum.inlₗ a₁) (sum.inlₗ a₂) = finset.map (function.embedding.inl.trans to_lex.to_embedding) (finset.Ico a₁ a₂)
theorem
sum.lex.Ioc_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Ioc (sum.inlₗ a₁) (sum.inlₗ a₂) = finset.map (function.embedding.inl.trans to_lex.to_embedding) (finset.Ioc a₁ a₂)
theorem
sum.lex.Ioo_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ a₂ : α) :
finset.Ioo (sum.inlₗ a₁) (sum.inlₗ a₂) = finset.map (function.embedding.inl.trans to_lex.to_embedding) (finset.Ioo a₁ a₂)
@[simp]
theorem
sum.lex.Icc_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Icc (sum.inlₗ a) (sum.inrₗ b) = finset.map to_lex.to_embedding ((finset.Ici a).disj_sum (finset.Iic b))
@[simp]
theorem
sum.lex.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Ico (sum.inlₗ a) (sum.inrₗ b) = finset.map to_lex.to_embedding ((finset.Ici a).disj_sum (finset.Iio b))
@[simp]
theorem
sum.lex.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Ioc (sum.inlₗ a) (sum.inrₗ b) = finset.map to_lex.to_embedding ((finset.Ioi a).disj_sum (finset.Iic b))
@[simp]
theorem
sum.lex.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Ioo (sum.inlₗ a) (sum.inrₗ b) = finset.map to_lex.to_embedding ((finset.Ioi a).disj_sum (finset.Iio b))
@[simp]
theorem
sum.lex.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Icc (sum.inrₗ b) (sum.inlₗ a) = ∅
@[simp]
theorem
sum.lex.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Ico (sum.inrₗ b) (sum.inlₗ a) = ∅
@[simp]
theorem
sum.lex.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Ioc (sum.inrₗ b) (sum.inlₗ a) = ∅
@[simp]
theorem
sum.lex.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(a : α)
(b : β) :
finset.Ioo (sum.inrₗ b) (sum.inlₗ a) = ∅
theorem
sum.lex.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Icc (sum.inrₗ b₁) (sum.inrₗ b₂) = finset.map (function.embedding.inr.trans to_lex.to_embedding) (finset.Icc b₁ b₂)
theorem
sum.lex.Ico_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ico (sum.inrₗ b₁) (sum.inrₗ b₂) = finset.map (function.embedding.inr.trans to_lex.to_embedding) (finset.Ico b₁ b₂)
theorem
sum.lex.Ioc_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ioc (sum.inrₗ b₁) (sum.inrₗ b₂) = finset.map (function.embedding.inr.trans to_lex.to_embedding) (finset.Ioc b₁ b₂)
theorem
sum.lex.Ioo_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[order_top α]
[order_bot β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ioo (sum.inrₗ b₁) (sum.inrₗ b₂) = finset.map (function.embedding.inr.trans to_lex.to_embedding) (finset.Ioo b₁ b₂)