Theorems · Theorem · combinatorics

AhlswedeZhang.supSum_singleton

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

Defined in

Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNonempty