powersetCard_eq_filter — Mathlib

English

The set of n-element subsets of s equals the filter of powerset s by membership of card = n.

Русский

Множество подмножеств s размерности n равно фильтру подмножеств s по условию card = n.

LaTeX

$$powersetCard n s = (powerset s).filter (fun x => x.card = n)$$

Lean4

theorem powersetCard_eq_filter {n} {s : Finset α} : powersetCard n s = (powerset s).filter fun x => x.card = n :=
  by
  ext
  simp [mem_powersetCard]

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