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.
instance
Pi.instLocallyFiniteOrderForAllPreorderToPreorder
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
:
LocallyFiniteOrder ((i : ι) → α i)
theorem
Pi.Icc_eq
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.Icc a b = Fintype.piFinset fun i => Finset.Icc (a i) (b i)
theorem
Pi.card_Icc
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.card (Finset.Icc a b) = Finset.prod Finset.univ fun i => Finset.card (Finset.Icc (a i) (b i))
theorem
Pi.card_Ico
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.card (Finset.Ico a b) = (Finset.prod Finset.univ fun i => Finset.card (Finset.Icc (a i) (b i))) - 1
theorem
Pi.card_Ioc
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.card (Finset.Ioc a b) = (Finset.prod Finset.univ fun i => Finset.card (Finset.Icc (a i) (b i))) - 1
theorem
Pi.card_Ioo
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.card (Finset.Ioo a b) = (Finset.prod Finset.univ fun i => Finset.card (Finset.Icc (a i) (b i))) - 2
instance
Pi.instLocallyFiniteOrderBotForAllPreorderToPreorder
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrderBot (α i)]
:
LocallyFiniteOrderBot ((i : ι) → α i)
theorem
Pi.card_Iic
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrderBot (α i)]
(b : (i : ι) → α i)
:
Finset.card (Finset.Iic b) = Finset.prod Finset.univ fun i => Finset.card (Finset.Iic (b i))
theorem
Pi.card_Iio
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrderBot (α i)]
(b : (i : ι) → α i)
:
Finset.card (Finset.Iio b) = (Finset.prod Finset.univ fun i => Finset.card (Finset.Iic (b i))) - 1
instance
Pi.instLocallyFiniteOrderTopForAllPreorderToPreorder
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrderTop (α i)]
:
LocallyFiniteOrderTop ((i : ι) → α i)
theorem
Pi.card_Ici
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrderTop (α i)]
(a : (i : ι) → α i)
:
Finset.card (Finset.Ici a) = Finset.prod Finset.univ fun i => Finset.card (Finset.Ici (a i))
theorem
Pi.card_Ioi
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → LocallyFiniteOrderTop (α i)]
(a : (i : ι) → α i)
:
Finset.card (Finset.Ioi a) = (Finset.prod Finset.univ fun i => Finset.card (Finset.Ici (a i))) - 1
theorem
Pi.uIcc_eq
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → Lattice (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.uIcc a b = Fintype.piFinset fun i => Finset.uIcc (a i) (b i)
theorem
Pi.card_uIcc
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
[(i : ι) → Lattice (α i)]
[(i : ι) → LocallyFiniteOrder (α i)]
(a : (i : ι) → α i)
(b : (i : ι) → α i)
:
Finset.card (Finset.uIcc a b) = Finset.prod Finset.univ fun i => Finset.card (Finset.uIcc (a i) (b i))