mathlib3 documentation

data.pi.interval

Intervals in a pi type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, instance]
def pi.locally_finite_order {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] :
locally_finite_order (Π (i : ι), α i)
Equations
source
theorem pi.Icc_eq {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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))
source
theorem pi.card_Icc {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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)
source
theorem pi.card_Ico {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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
source
theorem pi.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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
source
theorem pi.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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
source
@[protected, instance]
def pi.locally_finite_order_bot {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_bot (α i)] :
locally_finite_order_bot (Π (i : ι), α i)
Equations
source
theorem pi.card_Iic {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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)
source
theorem pi.card_Iio {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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
source
@[protected, instance]
def pi.locally_finite_order_top {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order_top (α i)] :
locally_finite_order_top (Π (i : ι), α i)
Equations
source
theorem pi.card_Ici {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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)
source
theorem pi.card_Ioi {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (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
source
theorem pi.uIcc_eq {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), lattice (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Π (i : ι), α i) :
finset.uIcc a b = fintype.pi_finset (λ (i : ι), finset.uIcc (a i) (b i))
source
theorem pi.card_uIcc {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), lattice (α i)] [Π (i : ι), locally_finite_order (α i)] (a b : Π (i : ι), α i) :
(finset.uIcc a b).card = finset.univ.prod (λ (i : ι), (finset.uIcc (a i) (b i)).card)