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} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] : LocallyFiniteOrder ((i : ι) → α i)

Equations

• Pi.instLocallyFiniteOrder = LocallyFiniteOrder.ofIcc ((i : ι) → α i) (fun (a b : (i : ι) → α i) => Fintype.piFinset fun (i : ι) => Finset.Icc (a i) (b i)) ⋯

theorem Pi.Icc_eq {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a 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 b : (i : ι) → α i) : (Finset.Icc a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card

theorem Pi.card_Ico {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i) : (Finset.Ico a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card - 1

theorem Pi.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i) : (Finset.Ioc a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card - 1

theorem Pi.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i) : (Finset.Ioo a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card - 2

instance Pi.instLocallyFiniteOrderBot {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrderBot (α i)] : LocallyFiniteOrderBot ((i : ι) → α i)

Equations

• Pi.instLocallyFiniteOrderBot = LocallyFiniteOrderBot.ofIic ((i : ι) → α i) (fun (b : (i : ι) → α i) => Fintype.piFinset fun (i : ι) => Finset.Iic (b 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.Iic b).card = ∏ i : ι, (Finset.Iic (b i)).card

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.Iio b).card = ∏ i : ι, (Finset.Iic (b i)).card - 1

instance Pi.instLocallyFiniteOrderTop {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrderTop (α i)] : LocallyFiniteOrderTop ((i : ι) → α i)

Equations

• Pi.instLocallyFiniteOrderTop = LocallyFiniteOrderTop.ofIci ((i : ι) → α i) (fun (a : (i : ι) → α i) => Fintype.piFinset fun (i : ι) => Finset.Ici (a 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.Ici a).card = ∏ i : ι, (Finset.Ici (a i)).card

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.Ioi a).card = ∏ i : ι, (Finset.Ici (a i)).card - 1

theorem Pi.uIcc_eq {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Lattice (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (a 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 b : (i : ι) → α i) : (Finset.uIcc a b).card = ∏ i : ι, (Finset.uIcc (a i) (b i)).card