powersetCard — Mathlib

English

PowersetCard(n,s) is the Finset of subsets of s with exactly n elements.

Русский

PowersetCard(n,s) — финсет подмножеств s, имеющих ровно n элементов.

LaTeX

$${α : Type*, n : Nat, s : Finset α} → Finset (Finset α) : powersetCard(n,s) = { t ⊆ s : card t = n }$$

Lean4

/-- Given an integer `n` and a finset `s`, then `powersetCard n s` is the finset of subsets of `s`
of cardinality `n`. -/
def powersetCard (n : ℕ) (s : Finset α) : Finset (Finset α) :=
  ⟨((s.1.powersetCard n).pmap Finset.mk) fun _t h => nodup_of_le (mem_powersetCard.1 h).1 s.2,
    s.2.powersetCard.pmap fun _a _ha _b _hb => congr_arg Finset.val⟩

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