Theorems · Theorem · combinatorics

AhlswedeZhang.supSum_of_univ_notMem

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α],
  𝒜.Nonempty →
    Finset.univ ∉ 𝒜 → AhlswedeZhang.supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹

Defined in: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Cited by: 1 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites27

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

Finsetstatement and proof · cited by 13,712
Fintypestatement and proof · cited by 7,736
Finset.sumstatement and proof · cited by 5,195
Finset.univstatement and proof · cited by 3,473
Finset.cardproof · cited by 2,327
Fintype.cardstatement and proof · cited by 1,386
Finset.rangestatement and proof · cited by 1,341
Finset.Nonemptystatement and proof · cited by 1,001
Finset.imageproof · cited by 910
LT.lt.neproof · cited by 872
LE.le.trans_ltproof · cited by 795
add_sub_cancel_rightproof · cited by 187

Cited by1

Results whose statement or proof uses this declaration.

AhlswedeZhang.infSum_eq_oneproof · cited by 0