indiscrete — Mathlib

English

Let n be a natural number. The construction indiscrete(n) yields a partition of n into exactly one block; that is, the multiset of block sizes is {n}. In other words, the partition consists of a single block containing all n elements.

Русский

Пусть n — натуральное число. Конструкция indiscrete(n) задаёт разбиение числа n на ровно один блок; то есть множество размеров блоков равно {n}. Иными словами, разбиение состоит из одного блока, содержащего все n элементов.

LaTeX

$$$\\operatorname{Blocks}(\\operatorname{Indiscrete}(n)) = \\{n\\}$$$

Lean4

/-- The partition of exactly one part. -/
def indiscrete (n : ℕ) : Partition n :=
  ofSums n { n } rfl

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