mathlib documentation

data.pi.interval

Intervals in a pi type #

This file shows that (dependent) functions to locally finite orders equipped with the pointwise order are locally finite and calculates the cardinality of their intervals.

@[protected, instance]
def pi.locally_finite_order {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] :
locally_finite_order (Π (i : ι), α i)
Equations
theorem pi.card_Icc {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Π (i : ι), α i) :
(finset.Icc a b).card = finset.univ.prod (λ (i : ι), (finset.Icc (a i) (b i)).card)
theorem pi.card_Ico {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Π (i : ι), α i) :
(finset.Ico a b).card = finset.univ.prod (λ (i : ι), (finset.Icc (a i) (b i)).card) - 1
theorem pi.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Π (i : ι), α i) :
(finset.Ioc a b).card = finset.univ.prod (λ (i : ι), (finset.Icc (a i) (b i)).card) - 1
theorem pi.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Π (i : ι), α i) :
(finset.Ioo a b).card = finset.univ.prod (λ (i : ι), (finset.Icc (a i) (b i)).card) - 2