# Finite intervals in a sigma type #

This file provides the LocallyFiniteOrder 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 #

instance Sigma.instLocallyFiniteOrder {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] :
LocallyFiniteOrder ((i : ι) × α i)
Equations
• One or more equations did not get rendered due to their size.
theorem Sigma.card_Icc {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a : (i : ι) × α i) (b : (i : ι) × α i) :
().card = if h : a.fst = b.fst then (Finset.Icc (ha.snd) b.snd).card else 0
theorem Sigma.card_Ico {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a : (i : ι) × α i) (b : (i : ι) × α i) :
().card = if h : a.fst = b.fst then (Finset.Ico (ha.snd) b.snd).card else 0
theorem Sigma.card_Ioc {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a : (i : ι) × α i) (b : (i : ι) × α i) :
().card = if h : a.fst = b.fst then (Finset.Ioc (ha.snd) b.snd).card else 0
theorem Sigma.card_Ioo {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a : (i : ι) × α i) (b : (i : ι) × α i) :
().card = if h : a.fst = b.fst then (Finset.Ioo (ha.snd) b.snd).card else 0
@[simp]
theorem Sigma.Icc_mk_mk {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :
Finset.Icc i, a i, b =
@[simp]
theorem Sigma.Ico_mk_mk {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :
Finset.Ico i, a i, b =
@[simp]
theorem Sigma.Ioc_mk_mk {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :
Finset.Ioc i, a i, b =
@[simp]
theorem Sigma.Ioo_mk_mk {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :
Finset.Ioo i, a i, b =