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.

Equations

• Finset.sumLift₂ f g (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f a b)
• Finset.sumLift₂ f g (Sum.inl val) (Sum.inr val_1) = ∅
• Finset.sumLift₂ f g (Sum.inr val) (Sum.inl val_1) = ∅
• Finset.sumLift₂ f g (Sum.inr a) (Sum.inr b) = Finset.map Function.Embedding.inr (g a b)

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₂_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 : β₁ ⊕ β₂} : (sumLift₂ 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.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 : β₁ ⊕ β₂) : sumLift₂ f₁ f₂ a b ⊆ sumLift₂ g₁ g₂ 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.

Equations

• Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f₁ a b)
• Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) (Sum.inr val_1) = (g₁ val val_1).disjSum (g₂ val val_1)
• Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) (Sum.inl val_1) = ∅
• Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = Finset.map { toFun := Sum.inr, inj' := ⋯ } (f₂ a b)

@[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

@[instance_reducible]

instance Sum.instLocallyFiniteOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] : LocallyFiniteOrder (α ⊕ β)

Equations

• One or more equations did not get rendered due to their size.

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₂)

@[instance_reducible]

instance Sum.instLocallyFiniteOrderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] : LocallyFiniteOrderBot (α ⊕ β)

Equations

• One or more equations did not get rendered due to their size.

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)

@[instance_reducible]

instance Sum.instLocallyFiniteOrderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderTop α] [LocallyFiniteOrderTop β] : LocallyFiniteOrderTop (α ⊕ β)

Equations

• One or more equations did not get rendered due to their size.

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

@[instance_reducible]

instance Sum.Lex.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot β] : LocallyFiniteOrder (α ⊕ₗ β)

Equations

• One or more equations did not get rendered due to their size.

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₂)

@[instance_reducible]

instance Sum.Lex.instLocallyFiniteOrderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [Fintype α] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] : LocallyFiniteOrderBot (α ⊕ₗ β)

Equations

• One or more equations did not get rendered due to their size.

theorem Sum.Lex.Iic_inl {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [Fintype α] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] (a : α) : Finset.Iic (inlₗ a) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Iic 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 : α) : Finset.Iio (inlₗ a) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Iio 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))

@[instance_reducible]

instance Sum.Lex.instLocallyFiniteOrderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderTop α] [Fintype β] [LocallyFiniteOrderTop β] : LocallyFiniteOrderTop (α ⊕ₗ β)

Equations

• One or more equations did not get rendered due to their size.

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 : β) : Finset.Ici (inrₗ b) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ici 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 : β) : Finset.Ioi (inrₗ b) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioi b)