odds — Mathlib

English

The finset of those partitions in which every part is odd.

Русский

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

LaTeX

$$$\mathrm{odds}(n) = \{ c \in \mathrm{Partition}(n) \mid \forall i \in c.\mathrm{parts}, i \text{ is odd} \}$$$

Lean4

/-- The finset of those partitions in which every part is odd. -/
def odds (n : ℕ) : Finset (Partition n) :=
  Finset.univ.filter fun c => ∀ i ∈ c.parts, ¬Even i

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