memPartition_zero

Mathlib.Data.Set.MemPartition

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

English

At level 0, memPartition(f,0) consists of a single block, namely the whole space.

Русский

На уровне 0 memPartition(f,0) состоит из единственного блока — всего пространства.

LaTeX

$$$\\operatorname{memPartition}(f)(0) = \\{ \\operatorname{univ} \\}$$$

Lean4

@[simp]
theorem memPartition_zero (f : ℕ → Set α) : memPartition f 0 = { univ } :=
  rfl

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

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

Разделы

Аффилиация

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