# mathlib3documentation

data.sigma.interval

# 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
theorem sigma.card_Icc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Σ (i : ι), α i) :
b).card = dite (a.fst = b.fst) (λ (h : a.fst = b.fst), (finset.Icc (eq.rec a.snd h) b.snd).card) (λ (h : ¬a.fst = b.fst), 0)
theorem sigma.card_Ico {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Σ (i : ι), α i) :
b).card = dite (a.fst = b.fst) (λ (h : a.fst = b.fst), (finset.Ico (eq.rec a.snd h) b.snd).card) (λ (h : ¬a.fst = b.fst), 0)
theorem sigma.card_Ioc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Σ (i : ι), α i) :
b).card = dite (a.fst = b.fst) (λ (h : a.fst = b.fst), (finset.Ioc (eq.rec a.snd h) b.snd).card) (λ (h : ¬a.fst = b.fst), 0)
theorem sigma.card_Ioo {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Σ (i : ι), α i) :
b).card = dite (a.fst = b.fst) (λ (h : a.fst = b.fst), (finset.Ioo (eq.rec a.snd h) b.snd).card) (λ (h : ¬a.fst = b.fst), 0)
@[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⟩ =
@[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⟩ =
@[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⟩ =
@[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⟩ =