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
• One or more equations did not get rendered due to their size.
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 Finset.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₁ Finset.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₂ Finset.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 : β₁ β₂} :
Finset.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 : β₁ β₂} :
(Finset.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₁ : α₁β₁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
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
• One or more equations did not get rendered due to their size.
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 : β₁) :
Finset.sumLexLift f₁ f₂ g₁ g₂ () () = Finset.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 : β₂) :
Finset.sumLexLift f₁ f₂ g₁ g₂ () () = (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 : β₁) :
Finset.sumLexLift f₁ f₂ g₁ g₂ () () =
@[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 : β₂) :
Finset.sumLexLift f₁ f₂ g₁ g₂ () () = Finset.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 Finset.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₁ Finset.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₂ Finset.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₁ : α₁β₁Finset γ₁} {f₁' : α₁β₁Finset γ₁} {f₂ : α₂β₂Finset γ₂} {f₂' : α₂β₂Finset γ₂} {g₁ : α₁β₂Finset γ₁} {g₁' : α₁β₂Finset γ₁} {g₂ : α₁β₂Finset γ₂} {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 : β₁ β₂) :
Finset.sumLexLift f₁ f₂ g₁ g₂ a b Finset.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 : β₁ β₂} :
Finset.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 : β₁ β₂} :
(Finset.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 Sum.instLocallyFiniteOrder {α : Type u_1} {β : Type u_2} [] [] :
Equations
• One or more equations did not get rendered due to their size.
theorem Sum.Icc_inl_inl {α : Type u_1} {β : Type u_2} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (a₁ : α) (b₂ : β) :
@[simp]
theorem Sum.Ico_inl_inr {α : Type u_1} {β : Type u_2} [] [] (a₁ : α) (b₂ : β) :
@[simp]
theorem Sum.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [] [] (a₁ : α) (b₂ : β) :
@[simp]
theorem Sum.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [] [] (a₁ : α) (b₂ : β) :
@[simp]
theorem Sum.Icc_inr_inl {α : Type u_1} {β : Type u_2} [] [] (a₂ : α) (b₁ : β) :
@[simp]
theorem Sum.Ico_inr_inl {α : Type u_1} {β : Type u_2} [] [] (a₂ : α) (b₁ : β) :
@[simp]
theorem Sum.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [] [] (a₂ : α) (b₁ : β) :
@[simp]
theorem Sum.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [] [] (a₂ : α) (b₁ : β) :
theorem Sum.Icc_inr_inr {α : Type u_1} {β : Type u_2} [] [] (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} [] [] (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} [] [] (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} [] [] (b₁ : β) (b₂ : β) :
Finset.Ioo (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioo b₁ b₂)

Lexicographical sum of orders #

instance Sum.Lex.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [] [] [] [] :
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} [] [] [] [] (a₁ : α) (a₂ : α) :
Finset.Icc (Sum.inlₗ a₁) (Sum.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} [] [] [] [] (a₁ : α) (a₂ : α) :
Finset.Ico (Sum.inlₗ a₁) (Sum.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} [] [] [] [] (a₁ : α) (a₂ : α) :
Finset.Ioc (Sum.inlₗ a₁) (Sum.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} [] [] [] [] (a₁ : α) (a₂ : α) :
Finset.Ioo (Sum.inlₗ a₁) (Sum.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} [] [] [] [] (a : α) (b : β) :
Finset.Icc () () = Finset.map toLex.toEmbedding (().disjSum ())
@[simp]
theorem Sum.Lex.Ico_inl_inr {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
Finset.Ico () () = Finset.map toLex.toEmbedding (().disjSum ())
@[simp]
theorem Sum.Lex.Ioc_inl_inr {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
Finset.Ioc () () = Finset.map toLex.toEmbedding (().disjSum ())
@[simp]
theorem Sum.Lex.Ioo_inl_inr {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
Finset.Ioo () () = Finset.map toLex.toEmbedding (().disjSum ())
@[simp]
theorem Sum.Lex.Icc_inr_inl {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
@[simp]
theorem Sum.Lex.Ico_inr_inl {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
@[simp]
theorem Sum.Lex.Ioc_inr_inl {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
@[simp]
theorem Sum.Lex.Ioo_inr_inl {α : Type u_1} {β : Type u_2} [] [] [] [] (a : α) (b : β) :
theorem Sum.Lex.Icc_inr_inr {α : Type u_1} {β : Type u_2} [] [] [] [] (b₁ : β) (b₂ : β) :
Finset.Icc (Sum.inrₗ b₁) (Sum.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} [] [] [] [] (b₁ : β) (b₂ : β) :
Finset.Ico (Sum.inrₗ b₁) (Sum.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} [] [] [] [] (b₁ : β) (b₂ : β) :
Finset.Ioc (Sum.inrₗ b₁) (Sum.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} [] [] [] [] (b₁ : β) (b₂ : β) :
Finset.Ioo (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioo b₁ b₂)