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 γ₂)
:
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.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 γ₂)
:
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₂ (Sum.inl a) (Sum.inl b) = 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₂ (Sum.inl a) (Sum.inr b) = Finset.disjSum (g₁ a b) (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₂ (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 : β₂)
:
Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = 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.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_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}
[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 (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₂)
Lexicographical sum of orders #
instance
Sum.Lex.locallyFiniteOrder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
:
LocallyFiniteOrder (Lex (α ⊕ β))
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 β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(a₂ : α)
:
Finset.Icc (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.trans Function.Embedding.inl (Equiv.toEmbedding toLex)) (Finset.Icc a₁ a₂)
theorem
Sum.Lex.Ico_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(a₂ : α)
:
Finset.Ico (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.trans Function.Embedding.inl (Equiv.toEmbedding toLex)) (Finset.Ico a₁ a₂)
theorem
Sum.Lex.Ioc_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(a₂ : α)
:
Finset.Ioc (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.trans Function.Embedding.inl (Equiv.toEmbedding toLex)) (Finset.Ioc a₁ a₂)
theorem
Sum.Lex.Ioo_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(a₂ : α)
:
Finset.Ioo (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.trans Function.Embedding.inl (Equiv.toEmbedding toLex)) (Finset.Ioo a₁ a₂)
@[simp]
theorem
Sum.Lex.Icc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Icc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map (Equiv.toEmbedding toLex) (Finset.disjSum (Finset.Ici a) (Finset.Iic b))
@[simp]
theorem
Sum.Lex.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Ico (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map (Equiv.toEmbedding toLex) (Finset.disjSum (Finset.Ici a) (Finset.Iio b))
@[simp]
theorem
Sum.Lex.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Ioc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map (Equiv.toEmbedding toLex) (Finset.disjSum (Finset.Ioi a) (Finset.Iic b))
@[simp]
theorem
Sum.Lex.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Ioo (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map (Equiv.toEmbedding toLex) (Finset.disjSum (Finset.Ioi a) (Finset.Iio b))
@[simp]
theorem
Sum.Lex.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Icc (Sum.inrₗ b) (Sum.inlₗ a) = ∅
@[simp]
theorem
Sum.Lex.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Ico (Sum.inrₗ b) (Sum.inlₗ a) = ∅
@[simp]
theorem
Sum.Lex.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Ioc (Sum.inrₗ b) (Sum.inlₗ a) = ∅
@[simp]
theorem
Sum.Lex.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a : α)
(b : β)
:
Finset.Ioo (Sum.inrₗ b) (Sum.inlₗ a) = ∅
theorem
Sum.Lex.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ : β)
(b₂ : β)
:
Finset.Icc (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.trans Function.Embedding.inr (Equiv.toEmbedding toLex)) (Finset.Icc b₁ b₂)
theorem
Sum.Lex.Ico_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ : β)
(b₂ : β)
:
Finset.Ico (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.trans Function.Embedding.inr (Equiv.toEmbedding toLex)) (Finset.Ico b₁ b₂)
theorem
Sum.Lex.Ioc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ : β)
(b₂ : β)
:
Finset.Ioc (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.trans Function.Embedding.inr (Equiv.toEmbedding toLex)) (Finset.Ioc b₁ b₂)
theorem
Sum.Lex.Ioo_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[OrderTop α]
[OrderBot β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ : β)
(b₂ : β)
:
Finset.Ioo (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.trans Function.Embedding.inr (Equiv.toEmbedding toLex)) (Finset.Ioo b₁ b₂)