eq

Mathlib.Data.Setoid.Partition

URI: https://scilib.ai/kg/mathlib#IndexedPartition.eq

English

Each block s_i equals the set of elements whose index is i.

Русский

Каждый блок s_i равен множеству элементов, чьи индексы равны i.

LaTeX

$$$s_i = \\{ x \\mid hs.index x = i \\}$$$

Lean4

theorem eq (i) : s i = {x | hs.index x = i} :=
  Set.ext fun _ => hs.mem_iff_index_eq

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

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

Разделы

Аффилиация

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