Documentation

Mathlib.Data.Sum.Interval

Finite intervals in a disjoint union #

This file provides the LocallyFiniteOrder instance for the disjoint sum of two orders.

TODO #

Do the same for the lexicographic sum of orders.

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.

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.Nonempty (Finset.sumLift₂ f g a b) (a₁ b₁, a = Sum.inl a₁ b = Sum.inl b₁ Finset.Nonempty (f a₁ b₁)) a₂ b₂, a = Sum.inr a₂ b = Sum.inr b₂ Finset.Nonempty (g a₂ b₂)
    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

    Disjoint sum of orders #

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