mathlib documentation

data.sum.interval

Finite intervals in a disjoint union #

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

TODO #

Do the same for the lexicographic sum of orders.

@[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 : β₁ β₂) :
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
theorem finset.mem_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 : β₁ β₂} {c : γ₁ γ₂} :
c finset.sum_lift₂ 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_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 : β₁ β₂} {c₁ : γ₁} :
sum.inl c₁ finset.sum_lift₂ f g a b ∃ (a₁ : α₁) (b₁ : β₁), a = sum.inl a₁ b = sum.inl b₁ c₁ f a₁ b₁
theorem finset.inr_mem_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 : β₁ β₂} {c₂ : γ₂} :
sum.inr c₂ finset.sum_lift₂ f g a b ∃ (a₂ : α₂) (b₂ : β₂), a = sum.inr a₂ b = sum.inr b₂ c₂ g a₂ b₂
theorem finset.sum_lift₂_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.sum_lift₂ 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.sum_lift₂_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.sum_lift₂ 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.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

Disjoint sum of orders #

theorem sum.Icc_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ a₂ : α) :
theorem sum.Ico_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ a₂ : α) :
theorem sum.Ioc_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ a₂ : α) :
theorem sum.Ioo_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ a₂ : α) :
@[simp]
theorem sum.Icc_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Ico_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Icc_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₂ : α) (b₁ : β) :
@[simp]
theorem sum.Ico_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₂ : α) (b₁ : β) :
@[simp]
theorem sum.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₂ : α) (b₁ : β) :
@[simp]
theorem sum.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (a₂ : α) (b₁ : β) :
theorem sum.Icc_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (b₁ b₂ : β) :
theorem sum.Ico_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (b₁ b₂ : β) :
theorem sum.Ioc_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (b₁ b₂ : β) :
theorem sum.Ioo_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] (b₁ b₂ : β) :