# mathlib3documentation

data.sum.interval

# 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 : β₁ β₂) :
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 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₁ 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₂ 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 : β₁ β₂} :
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 : β₁ β₂} :
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 : β₁ β₂) :
f₂ a b 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 : β₁ β₂) :
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
@[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 : β₁) :
f₂ g₁ g₂ (sum.inl a) (sum.inl b) = (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 : β₂) :
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 : β₁) :
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 : β₂) :
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 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_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₁ : γ₁} :
sum.inl c₁ 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_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₂ : γ₂} :
sum.inr c₂ 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.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 : β₁ β₂) :
f₂ g₁ g₂ a b f₂' g₁' g₂' a b
theorem finset.sum_lex_lift_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 : β₁ β₂} :
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.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 : β₁ β₂} :
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 β]  :
Equations
theorem sum.Icc_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ a₂ : α) :
finset.Icc (sum.inl a₁) (sum.inl a₂) =
theorem sum.Ico_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ a₂ : α) :
finset.Ico (sum.inl a₁) (sum.inl a₂) =
theorem sum.Ioc_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ a₂ : α) :
finset.Ioc (sum.inl a₁) (sum.inl a₂) =
theorem sum.Ioo_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ a₂ : α) :
finset.Ioo (sum.inl a₁) (sum.inl a₂) =
@[simp]
theorem sum.Icc_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Ico_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ : α) (b₂ : β) :
@[simp]
theorem sum.Icc_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₂ : α) (b₁ : β) :
@[simp]
theorem sum.Ico_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₂ : α) (b₁ : β) :
@[simp]
theorem sum.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₂ : α) (b₁ : β) :
@[simp]
theorem sum.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₂ : α) (b₁ : β) :
theorem sum.Icc_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (b₁ b₂ : β) :
finset.Icc (sum.inr b₁) (sum.inr b₂) =
theorem sum.Ico_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (b₁ b₂ : β) :
finset.Ico (sum.inr b₁) (sum.inr b₂) =
theorem sum.Ioc_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (b₁ b₂ : β) :
finset.Ioc (sum.inr b₁) (sum.inr b₂) =
theorem sum.Ioo_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (b₁ b₂ : β) :
finset.Ioo (sum.inr b₁) (sum.inr 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 β]  :
Equations
theorem sum.lex.Icc_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a₁ a₂ : α) :
theorem sum.lex.Ico_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a₁ a₂ : α) :
theorem sum.lex.Ioc_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a₁ a₂ : α) :
theorem sum.lex.Ioo_inl_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a₁ a₂ : α) :
@[simp]
theorem sum.lex.Icc_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Ico_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Icc_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Ico_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
@[simp]
theorem sum.lex.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (a : α) (b : β) :
theorem sum.lex.Icc_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (b₁ b₂ : β) :
theorem sum.lex.Ico_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (b₁ b₂ : β) :
theorem sum.lex.Ioc_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (b₁ b₂ : β) :
theorem sum.lex.Ioo_inr_inr {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top α] [order_bot β] (b₁ b₂ : β) :