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.instLocallyFiniteOrderSigmaPreorder {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(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} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a : (i : ι) × α i) (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 : (i : ι) × α i) (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 : (i : ι) × α i) (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 : (i : ι) × α i) (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 : α i) (b : α i) : Finset.Icc { fst := i, snd := a } { fst := i, snd := 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 : α i) (b : α i) : Finset.Ico { fst := i, snd := a } { fst := i, snd := 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 : α i) (b : α i) : Finset.Ioc { fst := i, snd := a } { fst := i, snd := 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 : α i) (b : α i) : Finset.Ioo { fst := i, snd := a } { fst := i, snd := b } = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioo a b)