instFinite_memPartition

Mathlib.Data.Set.MemPartition

URI: https://scilib.ai/kg/mathlib#instFinite_memPartition

English

For any f and n, memPartition(f,n) is finite (as a collection of blocks).

Русский

Для любых f и n memPartition(f,n) является конечной коллекцией блоков.

LaTeX

$$For all f,n, memPartition(f,n).Finite$$

Lean4

instance instFinite_memPartition (f : ℕ → Set α) (n : ℕ) : Finite (memPartition f n) :=
  Set.finite_coe_iff.mp (finite_memPartition _ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru