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