finite_countablePartition — Mathlib

English

countablePartition α n is a finite partition, i.e., it has finitely many blocks.

Русский

countablePartition α n является конечным разбиением, то есть содержит конечное число блоков.

LaTeX

$$$\text{countablePartition}(\alpha,n)\text{ is finite}$$$

Lean4

theorem finite_countablePartition (α : Type*) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) :
    Set.Finite (countablePartition α n) :=
  finite_memPartition _ n

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