Documentation

Mathlib.Data.Sigma.Interval

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)
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 (ha.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 (ha.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 (ha.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 (ha.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) :
@[simp]
theorem Sigma.Ico_mk_mk {ι : Type u_1} {α : ιType u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :
@[simp]
theorem Sigma.Ioc_mk_mk {ι : Type u_1} {α : ιType u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :
@[simp]
theorem Sigma.Ioo_mk_mk {ι : Type u_1} {α : ιType u_2} [DecidableEq ι] [(i : ι) → Preorder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a : α i) (b : α i) :