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.Icc_eq {ι : 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 = fintype.pi_finset (λ (i : ι), finset.Icc (a i) (b i))
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
@[protected, instance]
def pi.locally_finite_order_bot {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_bot (α i)] :
locally_finite_order_bot (Π (i : ι), α i)
Equations
theorem pi.card_Iic {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_bot (α i)] (b : Π (i : ι), α i) :
(finset.Iic b).card = finset.univ.prod (λ (i : ι), (finset.Iic (b i)).card)
theorem pi.card_Iio {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_bot (α i)] (b : Π (i : ι), α i) :
(finset.Iio b).card = finset.univ.prod (λ (i : ι), (finset.Iic (b i)).card) - 1
@[protected, instance]
def pi.locally_finite_order_top {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_top (α i)] :
locally_finite_order_top (Π (i : ι), α i)
Equations
theorem pi.card_Ici {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_top (α i)] (a : Π (i : ι), α i) :
(finset.Ici a).card = finset.univ.prod (λ (i : ι), (finset.Ici (a i)).card)
theorem pi.card_Ioi {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [fintype ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_top (α i)] (a : Π (i : ι), α i) :
(finset.Ioi a).card = finset.univ.prod (λ (i : ι), (finset.Ici (a i)).card) - 1