Theorems · Theorem · order theory

Pi.card_uIcc

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

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: Fintype DecidableEq DecidableEq Lattice LocallyFiniteOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fintypestatement and proof · cited by 7,736
Finset.univstatement · cited by 3,473
Finset.prodstatement · cited by 2,356
Finset.cardstatement · cited by 2,327
Latticestatement and proof · cited by 916
LocallyFiniteOrderstatement and proof · cited by 658
Finset.uIccstatement · cited by 84
Pi.card_Iccproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.