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 γ₂)
:
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.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₂)