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} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] : LocallyFiniteOrder ((i : ι) × α i)

theorem Sigma.card_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i) : (Finset.Icc a b).card = if h : a.fst = b.fst then (Finset.Icc (h ▸ a.snd) b.snd).card else 0

theorem Sigma.card_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i) : (Finset.Ico a b).card = if h : a.fst = b.fst then (Finset.Ico (h ▸ a.snd) b.snd).card else 0

theorem Sigma.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i) : (Finset.Ioc a b).card = if h : a.fst = b.fst then (Finset.Ioc (h ▸ a.snd) b.snd).card else 0

theorem Sigma.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i) : (Finset.Ioo a b).card = if h : a.fst = b.fst then (Finset.Ioo (h ▸ a.snd) b.snd).card else 0

@[simp]

theorem Sigma.Icc_mk_mk {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i) : Finset.Icc ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Icc a b)

@[simp]

theorem Sigma.Ico_mk_mk {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i) : Finset.Ico ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ico a b)

@[simp]

theorem Sigma.Ioc_mk_mk {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i) : Finset.Ioc ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioc a b)

@[simp]

theorem Sigma.Ioo_mk_mk {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i) : Finset.Ioo ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioo a b)

instance Sigma.instLocallyFiniteOrderBot {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrderBot (α i)] : LocallyFiniteOrderBot ((i : ι) × α i)

@[simp]

theorem Sigma.Iic_mk {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrderBot (α i)] (i : ι) (a : α i) : Finset.Iic ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Iic a)

@[simp]

theorem Sigma.Iio_mk {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrderBot (α i)] (i : ι) (a : α i) : Finset.Iio ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Iio a)

instance Sigma.instLocallyFiniteOrderTop {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrderTop (α i)] : LocallyFiniteOrderTop ((i : ι) × α i)

@[simp]

theorem Sigma.Ici_mk {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrderTop (α i)] (i : ι) (a : α i) : Finset.Ici ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ici a)

@[simp]

theorem Sigma.Ioi_mk {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrderTop (α i)] (i : ι) (a : α i) : Finset.Ioi ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioi a)