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 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 : β₁ ⊕ β₂) :
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
- finset.sum_lift₂ f g (sum.inr a) (sum.inr b) = finset.map function.embedding.inr (g a b)
- finset.sum_lift₂ f g (sum.inr a) (sum.inl b) = ∅
- finset.sum_lift₂ f g (sum.inl a) (sum.inr b) = ∅
- finset.sum_lift₂ f g (sum.inl a) (sum.inl b) = finset.map function.embedding.inl (f a b)
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 #
@[protected, instance]
def
sum.locally_finite_order
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β] :
locally_finite_order (α ⊕ β)
Equations
- sum.locally_finite_order = {finset_Icc := finset.sum_lift₂ finset.Icc finset.Icc, finset_Ico := finset.sum_lift₂ finset.Ico finset.Ico, finset_Ioc := finset.sum_lift₂ finset.Ioc finset.Ioc, finset_Ioo := finset.sum_lift₂ finset.Ioo finset.Ioo, finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
theorem
sum.Icc_inl_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Icc (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Ico (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Ioc (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₁ : α)
(b₂ : β) :
finset.Ioo (sum.inl a₁) (sum.inr b₂) = ∅
@[simp]
theorem
sum.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Icc (sum.inr b₁) (sum.inl a₂) = ∅
@[simp]
theorem
sum.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Ico (sum.inr b₁) (sum.inl a₂) = ∅
@[simp]
theorem
sum.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Ioc (sum.inr b₁) (sum.inl a₂) = ∅
@[simp]
theorem
sum.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(a₂ : α)
(b₁ : β) :
finset.Ioo (sum.inr b₁) (sum.inl a₂) = ∅
theorem
sum.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(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 β]
[locally_finite_order α]
[locally_finite_order β]
(b₁ b₂ : β) :
finset.Ioo (sum.inr b₁) (sum.inr b₂) = finset.map function.embedding.inr (finset.Ioo b₁ b₂)