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.

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

instance Sum.instLocallyFiniteOrderSumInstPreorderSum {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] : LocallyFiniteOrder (α ⊕ β)

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₂ : β) : Finset.Icc (Sum.inl a₁) (Sum.inr b₂) = ∅

@[simp]

theorem Sum.Ico_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) : Finset.Ico (Sum.inl a₁) (Sum.inr b₂) = ∅

@[simp]

theorem Sum.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) : Finset.Ioc (Sum.inl a₁) (Sum.inr b₂) = ∅

@[simp]

theorem Sum.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₁ : α) (b₂ : β) : Finset.Ioo (Sum.inl a₁) (Sum.inr b₂) = ∅

@[simp]

theorem Sum.Icc_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) : Finset.Icc (Sum.inr b₁) (Sum.inl a₂) = ∅

@[simp]

theorem Sum.Ico_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) : Finset.Ico (Sum.inr b₁) (Sum.inl a₂) = ∅

@[simp]

theorem Sum.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) : Finset.Ioc (Sum.inr b₁) (Sum.inl a₂) = ∅

@[simp]

theorem Sum.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] (a₂ : α) (b₁ : β) : Finset.Ioo (Sum.inr b₁) (Sum.inl a₂) = ∅

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