distincts — Mathlib

English

The finset of partitions in which every part is used at most once.

Русский

Множество разбиений, в котором каждая часть используется не более одного раза.

LaTeX

$$$\mathrm{distincts}(n) = \{ c \in \mathrm{Partition}(n) \mid \operatorname{Nodup}(c.\mathrm{parts}) \}$$$

Lean4

/-- The finset of those partitions in which each part is used at most once. -/
def distincts (n : ℕ) : Finset (Partition n) :=
  Finset.univ.filter fun c => c.parts.Nodup

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