Theorems · Theorem · order theory

DFinsupp.card_Icc

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), (Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card

Defined in

Mathlib.Data.DFinsupp.Interval

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqPartialOrderZeroLocallyFiniteOrder