Theorems · Theorem · order theory

Sigma.card_Ico

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i),
  (Finset.Ico a b).card = if h : a.fst = b.fst then (Finset.Ico (h ▸ a.snd) b.snd).card else 0

Defined in: Mathlib.Data.Sigma.Interval
Cited by: 0 results in Mathlib
Foundations: Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Preorder LocallyFiniteOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Preorderstatement and proof · cited by 7,952
Finset.cardstatement · cited by 2,327
LocallyFiniteOrderstatement and proof · cited by 658
Finset.Icostatement and proof · cited by 450
Finset.card_sigmaLiftproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.