oddDistincts — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{oddDistincts}(n) = \mathrm{odds}(n) \cap \mathrm{distincts}(n)$$$

Lean4

/-- The finset of those partitions in which every part is odd and used at most once. -/
def oddDistincts (n : ℕ) : Finset (Partition n) :=
  odds n ∩ distincts n

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