Documentation

Mathlib.Data.Sum.Interval

Finite intervals in a disjoint union #

This file provides the LocallyFiniteOrder instance for the disjoint sum and linear sum of two orders and calculates the cardinality of their finite intervals.

def Finset.sumLift₂ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (f : α₁β₁Finset γ₁) (g : α₂β₂Finset γ₂) :
α₁ α₂β₁ β₂Finset (γ₁ γ₂)

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
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Finset.mem_sumLift₂ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f : α₁β₁Finset γ₁} {g : α₂β₂Finset γ₂} {a : α₁ α₂} {b : β₁ β₂} {c : γ₁ γ₂} :
    c Finset.sumLift₂ f 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.inr a₂ b = Sum.inr b₂ c = Sum.inr c₂ c₂ g a₂ b₂
    theorem Finset.inl_mem_sumLift₂ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f : α₁β₁Finset γ₁} {g : α₂β₂Finset γ₂} {a : α₁ α₂} {b : β₁ β₂} {c₁ : γ₁} :
    Sum.inl c₁ Finset.sumLift₂ f g a b ∃ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ b = Sum.inl b₁ c₁ f a₁ b₁
    theorem Finset.inr_mem_sumLift₂ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f : α₁β₁Finset γ₁} {g : α₂β₂Finset γ₂} {a : α₁ α₂} {b : β₁ β₂} {c₂ : γ₂} :
    Sum.inr c₂ Finset.sumLift₂ f g a b ∃ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ b = Sum.inr b₂ c₂ g a₂ b₂
    theorem Finset.sumLift₂_eq_empty {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f : α₁β₁Finset γ₁} {g : α₂β₂Finset γ₂} {a : α₁ α₂} {b : β₁ β₂} :
    Finset.sumLift₂ f g a b = (∀ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁b = Sum.inl b₁f a₁ b₁ = ) ∀ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂b = Sum.inr b₂g a₂ b₂ =
    theorem Finset.sumLift₂_nonempty {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f : α₁β₁Finset γ₁} {g : α₂β₂Finset γ₂} {a : α₁ α₂} {b : β₁ β₂} :
    (Finset.sumLift₂ f g a b).Nonempty (∃ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ b = Sum.inl b₁ (f a₁ b₁).Nonempty) ∃ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ b = Sum.inr b₂ (g a₂ b₂).Nonempty
    theorem Finset.sumLift₂_mono {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f₁ : α₁β₁Finset γ₁} {g₁ : α₁β₁Finset γ₁} {f₂ : α₂β₂Finset γ₂} {g₂ : α₂β₂Finset γ₂} (h₁ : ∀ (a : α₁) (b : β₁), f₁ a b g₁ a b) (h₂ : ∀ (a : α₂) (b : β₂), f₂ a b g₂ a b) (a : α₁ α₂) (b : β₁ β₂) :
    Finset.sumLift₂ f₁ f₂ a b Finset.sumLift₂ g₁ g₂ a b
    def Finset.sumLexLift {α₁ : 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 γ₂) :
    α₁ α₂β₁ β₂Finset (γ₁ γ₂)

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Finset.sumLexLift_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.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f₁ a b)
      @[simp]
      theorem Finset.sumLexLift_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.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inr b) = (g₁ a b).disjSum (g₂ a b)
      @[simp]
      theorem Finset.sumLexLift_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.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inl b) =
      @[simp]
      theorem Finset.sumLexLift_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.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = Finset.map { toFun := Sum.inr, inj' := } (f₂ a b)
      theorem Finset.mem_sumLexLift {α₁ : 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.sumLexLift 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.inl_mem_sumLexLift {α₁ : 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₁ : γ₁} :
      Sum.inl c₁ Finset.sumLexLift f₁ f₂ g₁ g₂ a b (∃ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ b = Sum.inl b₁ c₁ f₁ a₁ b₁) ∃ (a₁ : α₁) (b₂ : β₂), a = Sum.inl a₁ b = Sum.inr b₂ c₁ g₁ a₁ b₂
      theorem Finset.inr_mem_sumLexLift {α₁ : 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₂ : γ₂} :
      Sum.inr c₂ Finset.sumLexLift f₁ f₂ g₁ g₂ a b (∃ (a₁ : α₁) (b₂ : β₂), a = Sum.inl a₁ b = Sum.inr b₂ c₂ g₂ a₁ b₂) ∃ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ b = Sum.inr b₂ c₂ f₂ a₂ b₂
      theorem Finset.sumLexLift_mono {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} {f₁ : α₁β₁Finset γ₁} {f₁' : α₁β₁Finset γ₁} {f₂ : α₂β₂Finset γ₂} {f₂' : α₂β₂Finset γ₂} {g₁ : α₁β₂Finset γ₁} {g₁' : α₁β₂Finset γ₁} {g₂ : α₁β₂Finset γ₂} {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.sumLexLift f₁ f₂ g₁ g₂ a b Finset.sumLexLift f₁' f₂' g₁' g₂' a b
      theorem Finset.sumLexLift_eq_empty {α₁ : 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.sumLexLift f₁ f₂ g₁ g₂ a b = (∀ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁b = Sum.inl b₁f₁ a₁ b₁ = ) (∀ (a₁ : α₁) (b₂ : β₂), a = Sum.inl a₁b = Sum.inr b₂g₁ a₁ b₂ = g₂ a₁ b₂ = ) ∀ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂b = Sum.inr b₂f₂ a₂ b₂ =
      theorem Finset.sumLexLift_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.sumLexLift 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 #

      Equations
      • One or more equations did not get rendered due to their size.
      theorem Sum.Icc_inl_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) :
      @[simp]
      theorem Sum.Ico_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) :
      @[simp]
      theorem Sum.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) :
      @[simp]
      theorem Sum.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) :
      @[simp]
      theorem Sum.Icc_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) :
      @[simp]
      theorem Sum.Ico_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) :
      @[simp]
      theorem Sum.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) :
      @[simp]
      theorem Sum.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) :
      theorem Sum.Icc_inr_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (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 β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (b₁ : β) (b₂ : β) :
      Finset.Ioo (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioo b₁ b₂)

      Lexicographical sum of orders #

      Equations
      • One or more equations did not get rendered due to their size.
      theorem Sum.Lex.Icc_inl_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (a₂ : α) :
      Finset.Icc (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Icc a₁ a₂)
      theorem Sum.Lex.Ico_inl_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (a₂ : α) :
      Finset.Ico (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ico a₁ a₂)
      theorem Sum.Lex.Ioc_inl_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (a₂ : α) :
      Finset.Ioc (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioc a₁ a₂)
      theorem Sum.Lex.Ioo_inl_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (a₂ : α) :
      Finset.Ioo (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioo a₁ a₂)
      @[simp]
      theorem Sum.Lex.Icc_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      Finset.Icc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iic b))
      @[simp]
      theorem Sum.Lex.Ico_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      Finset.Ico (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iio b))
      @[simp]
      theorem Sum.Lex.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      Finset.Ioc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iic b))
      @[simp]
      theorem Sum.Lex.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      Finset.Ioo (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iio b))
      @[simp]
      theorem Sum.Lex.Icc_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      @[simp]
      theorem Sum.Lex.Ico_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      @[simp]
      theorem Sum.Lex.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      @[simp]
      theorem Sum.Lex.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a : α) (b : β) :
      theorem Sum.Lex.Icc_inr_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (b₁ : β) (b₂ : β) :
      Finset.Icc (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Icc b₁ b₂)
      theorem Sum.Lex.Ico_inr_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (b₁ : β) (b₂ : β) :
      Finset.Ico (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ico b₁ b₂)
      theorem Sum.Lex.Ioc_inr_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (b₁ : β) (b₂ : β) :
      Finset.Ioc (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioc b₁ b₂)
      theorem Sum.Lex.Ioo_inr_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (b₁ : β) (b₂ : β) :
      Finset.Ioo (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioo b₁ b₂)