prod_powersetCard — Mathlib

English

For a fixed n, ∏ t∈powersetCard n s, f t = f(n)^{C(|s|, n)} where C is a binomial coefficient.

Русский

Для фиксированного n верно: ∏_{t∈powersetCard n s} f(t) = f(n)^{C(|s|, n)}.

LaTeX

$$$\\displaystyle \\prod_{t \\in \\mathrm{powersetCard}(n,s)} f(t) = f(n)^{\\binom{|s|}{n}}$$

Lean4

/-- A product over `Finset.powersetCard` which only depends on the size of the sets is constant. -/
@[to_additive /-- A sum over `Finset.powersetCard` which only depends on the size of the sets is constant. -/
    ]
theorem prod_powersetCard (n : ℕ) (s : Finset α) (f : ℕ → β) : ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n := by
  rw [prod_eq_pow_card, card_powersetCard]; rintro a ha; rw [(mem_powersetCard.1 ha).2]

Похожие утверждения