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
- 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)
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₁ 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 γ₂)
:
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)
Instances For
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.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 : β₁ ⊕ β₂)
:
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 (α ⊕ β)
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₂ : α)
:
theorem
Sum.Ico_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ a₂ : α)
:
theorem
Sum.Ioc_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ a₂ : α)
:
theorem
Sum.Ioo_inl_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ a₂ : α)
:
@[simp]
theorem
Sum.Icc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
@[simp]
theorem
Sum.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
@[simp]
theorem
Sum.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
@[simp]
theorem
Sum.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₁ : α)
(b₂ : β)
:
@[simp]
theorem
Sum.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
@[simp]
theorem
Sum.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
@[simp]
theorem
Sum.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
@[simp]
theorem
Sum.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(a₂ : α)
(b₁ : β)
:
theorem
Sum.Icc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ b₂ : β)
:
theorem
Sum.Ico_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ b₂ : β)
:
theorem
Sum.Ioc_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ b₂ : β)
:
theorem
Sum.Ioo_inr_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
(b₁ b₂ : β)
:
@[implicit_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 : α)
:
theorem
Sum.Iic_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(b : β)
:
theorem
Sum.Iio_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(a : α)
:
theorem
Sum.Iio_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(b : β)
:
@[implicit_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 : α)
:
theorem
Sum.Ici_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(b : β)
:
theorem
Sum.Ioi_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(a : α)
:
theorem
Sum.Ioi_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderTop β]
(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 (α ⊕ β))
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 : β)
:
@[simp]
theorem
Sum.Lex.Ico_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
@[simp]
theorem
Sum.Lex.Ioc_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
@[simp]
theorem
Sum.Lex.Ioo_inl_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
@[simp]
theorem
Sum.Lex.Icc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
@[simp]
theorem
Sum.Lex.Ico_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
@[simp]
theorem
Sum.Lex.Ioc_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
@[simp]
theorem
Sum.Lex.Ioo_inr_inl
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrder α]
[LocallyFiniteOrder β]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot β]
(a : α)
(b : β)
:
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 (α ⊕ β))
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 : α)
:
theorem
Sum.Lex.Iic_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[Fintype α]
[LocallyFiniteOrderBot α]
[LocallyFiniteOrderBot β]
(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 : β)
:
@[implicit_reducible]
instance
Sum.Lex.instLocallyFiniteOrderTop
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
:
LocallyFiniteOrderTop (_root_.Lex (α ⊕ β))
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 : α)
:
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 : α)
:
theorem
Sum.Lex.Ioi_inr
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[LocallyFiniteOrderTop α]
[Fintype β]
[LocallyFiniteOrderTop β]
(b : β)
: