Theorems · Theorem · order theory

Pi.card_Ioo

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  (Finset.Ioo a b).card = ∏ i, (Finset.Icc (a i) (b i)).card - 2

Defined in

Mathlib.Data.Pi.Interval

Cited by

0 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidableEqPartialOrderLocallyFiniteOrder