Finite intervals in a sigma type #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides the locally_finite_order instance for the disjoint sum of orders Σ i, α i and
calculates the cardinality of its finite intervals.
TODO #
Do the same for the lexicographical order
Disjoint sum of orders #
@[protected, instance]
def
sigma.locally_finite_order
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)] :
locally_finite_order (Σ (i : ι), α i)
Equations
- sigma.locally_finite_order = {finset_Icc := finset.sigma_lift (λ (_x : ι), finset.Icc), finset_Ico := finset.sigma_lift (λ (_x : ι), finset.Ico), finset_Ioc := finset.sigma_lift (λ (_x : ι), finset.Ioc), finset_Ioo := finset.sigma_lift (λ (_x : ι), finset.Ioo), finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
theorem
sigma.card_Icc
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(a b : Σ (i : ι), α i) :
theorem
sigma.card_Ico
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(a b : Σ (i : ι), α i) :
theorem
sigma.card_Ioc
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(a b : Σ (i : ι), α i) :
theorem
sigma.card_Ioo
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(a b : Σ (i : ι), α i) :
@[simp]
theorem
sigma.Icc_mk_mk
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(i : ι)
(a b : α i) :
finset.Icc ⟨i, a⟩ ⟨i, b⟩ = finset.map (function.embedding.sigma_mk i) (finset.Icc a b)
@[simp]
theorem
sigma.Ico_mk_mk
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(i : ι)
(a b : α i) :
finset.Ico ⟨i, a⟩ ⟨i, b⟩ = finset.map (function.embedding.sigma_mk i) (finset.Ico a b)
@[simp]
theorem
sigma.Ioc_mk_mk
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(i : ι)
(a b : α i) :
finset.Ioc ⟨i, a⟩ ⟨i, b⟩ = finset.map (function.embedding.sigma_mk i) (finset.Ioc a b)
@[simp]
theorem
sigma.Ioo_mk_mk
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), preorder (α i)]
[Π (i : ι), locally_finite_order (α i)]
(i : ι)
(a b : α i) :
finset.Ioo ⟨i, a⟩ ⟨i, b⟩ = finset.map (function.embedding.sigma_mk i) (finset.Ioo a b)