Finite intervals in a disjoint union #
This file provides the LocallyFiniteOrder instance for the disjoint sum and linear sum of two
orders and calculates the cardinality of their finite intervals.
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.
Instances For
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 ∈ 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₁ ∈ 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₂ ∈ 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 : β₁ ⊕ β₂}
:
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₂_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 : β₁ ⊕ β₂)
:
def
Finset.sumLexLift
{α₁ : 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 γ₂)
:
α₁ ⊕ α₂ → β₁ ⊕ β₂ → 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.
Instances For
@[simp]
theorem
Finset.sumLexLift_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 : β₁)
:
sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inl b) = map Function.Embedding.inl (f₁ a b)
@[simp]
theorem
Finset.sumLexLift_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 : β₂)
:
sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inr b) = (g₁ a b).disjSum (g₂ a b)
@[simp]
theorem
Finset.sumLexLift_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 : β₁)
:
sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inl b) = ∅
@[simp]
theorem
Finset.sumLexLift_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 : β₂)
:
sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = map { toFun := Sum.inr, inj' := ⋯ } (f₂ a b)
theorem
Finset.mem_sumLexLift
{α₁ : 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 ∈ sumLexLift f₁ 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_sumLexLift
{α₁ : 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₁ ∈ sumLexLift f₁ 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_sumLexLift
{α₁ : 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₂ ∈ sumLexLift f₁ 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.sumLexLift_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 : β₁ ⊕ β₂)
:
sumLexLift f₁ f₂ g₁ g₂ a b ⊆ sumLexLift f₁' f₂' g₁' g₂' a b
theorem
Finset.sumLexLift_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 : β₁ ⊕ β₂}
:
sumLexLift f₁ 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.sumLexLift_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 : β₁ ⊕ β₂}
:
(sumLexLift f₁ 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 #
@[implicit_reducible]
instance
Sum.instLocallyFiniteOrder
{α : 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 (inl a₁) (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 (inl a₁) (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 (inl a₁) (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 (inl a₁) (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 (inl a₁) (inr b₂) = ∅
@[simp]
theorem
Sum.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
Finset.Ico (inl a₁) (inr b₂) = ∅
@[simp]
theorem
Sum.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
Finset.Ioc (inl a₁) (inr b₂) = ∅
@[simp]
theorem
Sum.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
Finset.Ioo (inl a₁) (inr b₂) = ∅
@[simp]
theorem
Sum.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
Finset.Icc (inr b₁) (inl a₂) = ∅
@[simp]
theorem
Sum.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
Finset.Ico (inr b₁) (inl a₂) = ∅
@[simp]
theorem
Sum.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
Finset.Ioc (inr b₁) (inl a₂) = ∅
@[simp]
theorem
Sum.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
Finset.Ioo (inr b₁) (inl a₂) = ∅
theorem
Sum.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ b₂ : β)
:
Finset.Icc (inr b₁) (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 (inr b₁) (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 (inr b₁) (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 (inr b₁) (inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioo b₁ b₂)
@[implicit_reducible]
instance
Sum.instLocallyFiniteOrderBot
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
:
LocallyFiniteOrderBot (α ⊕ β)
theorem
Sum.Iic_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(a : α)
:
Finset.Iic (inl a) = Finset.map Function.Embedding.inl (Finset.Iic a)
theorem
Sum.Iic_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(b : β)
:
Finset.Iic (inr b) = Finset.map Function.Embedding.inr (Finset.Iic b)
theorem
Sum.Iio_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(a : α)
:
Finset.Iio (inl a) = Finset.map Function.Embedding.inl (Finset.Iio a)
theorem
Sum.Iio_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(b : β)
:
Finset.Iio (inr b) = Finset.map Function.Embedding.inr (Finset.Iio b)
@[implicit_reducible]
instance
Sum.instLocallyFiniteOrderTop
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
:
LocallyFiniteOrderTop (α ⊕ β)
theorem
Sum.Ici_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(a : α)
:
Finset.Ici (inl a) = Finset.map Function.Embedding.inl (Finset.Ici a)
theorem
Sum.Ici_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(b : β)
:
Finset.Ici (inr b) = Finset.map Function.Embedding.inr (Finset.Ici b)
theorem
Sum.Ioi_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(a : α)
:
Finset.Ioi (inl a) = Finset.map Function.Embedding.inl (Finset.Ioi a)
theorem
Sum.Ioi_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(b : β)
:
Finset.Ioi (inr b) = Finset.map Function.Embedding.inr (Finset.Ioi b)
Lexicographical sum of orders #
@[implicit_reducible]
instance
Sum.Lex.locallyFiniteOrder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
:
LocallyFiniteOrder (_root_.Lex (α ⊕ β))
theorem
Sum.Lex.Icc_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a₁ a₂ : α)
:
Finset.Icc (inlₗ a₁) (inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Icc a₁ a₂)
theorem
Sum.Lex.Ico_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a₁ a₂ : α)
:
Finset.Ico (inlₗ a₁) (inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ico a₁ a₂)
theorem
Sum.Lex.Ioc_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a₁ a₂ : α)
:
Finset.Ioc (inlₗ a₁) (inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioc a₁ a₂)
theorem
Sum.Lex.Ioo_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a₁ a₂ : α)
:
Finset.Ioo (inlₗ a₁) (inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioo a₁ a₂)
@[simp]
theorem
Sum.Lex.Icc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Icc (inlₗ a) (inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iic b))
@[simp]
theorem
Sum.Lex.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Ico (inlₗ a) (inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iio b))
@[simp]
theorem
Sum.Lex.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Ioc (inlₗ a) (inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iic b))
@[simp]
theorem
Sum.Lex.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Ioo (inlₗ a) (inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iio b))
@[simp]
theorem
Sum.Lex.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Icc (inrₗ b) (inlₗ a) = ∅
@[simp]
theorem
Sum.Lex.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Ico (inrₗ b) (inlₗ a) = ∅
@[simp]
theorem
Sum.Lex.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Ioc (inrₗ b) (inlₗ a) = ∅
@[simp]
theorem
Sum.Lex.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
Finset.Ioo (inrₗ b) (inlₗ a) = ∅
theorem
Sum.Lex.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(b₁ b₂ : β)
:
Finset.Icc (inrₗ b₁) (inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Icc b₁ b₂)
theorem
Sum.Lex.Ico_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(b₁ b₂ : β)
:
Finset.Ico (inrₗ b₁) (inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ico b₁ b₂)
theorem
Sum.Lex.Ioc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(b₁ b₂ : β)
:
Finset.Ioc (inrₗ b₁) (inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioc b₁ b₂)
theorem
Sum.Lex.Ioo_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(b₁ b₂ : β)
:
Finset.Ioo (inrₗ b₁) (inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioo b₁ b₂)
@[implicit_reducible]
instance
Sum.Lex.instLocallyFiniteOrderBot
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[Fintype α]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
:
LocallyFiniteOrderBot (_root_.Lex (α ⊕ β))
theorem
Sum.Lex.Iic_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[Fintype α]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(a : α)
:
theorem
Sum.Lex.Iic_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[Fintype α]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(b : β)
:
Finset.Iic (inrₗ b) = Finset.map toLex.toEmbedding (Finset.univ.disjSum (Finset.Iic b))
theorem
Sum.Lex.Iio_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[Fintype α]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(a : α)
:
theorem
Sum.Lex.Iio_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[Fintype α]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(b : β)
:
Finset.Iio (inrₗ b) = Finset.map toLex.toEmbedding (Finset.univ.disjSum (Finset.Iio b))
@[implicit_reducible]
instance
Sum.Lex.instLocallyFiniteOrderTop
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
:
LocallyFiniteOrderTop (_root_.Lex (α ⊕ β))
theorem
Sum.Lex.Ici_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
(a : α)
:
Finset.Ici (inlₗ a) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum Finset.univ)
theorem
Sum.Lex.Ici_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
(b : β)
:
theorem
Sum.Lex.Ioi_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
(a : α)
:
Finset.Ioi (inlₗ a) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum Finset.univ)
theorem
Sum.Lex.Ioi_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
(b : β)
: