some_index

Mathlib.Data.Setoid.Partition

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

English

The setoid relation relates an element to the representative of its block.

Русский

Отношение эквивалентности связывает элемент с представителем своего блока.

LaTeX

$$$ hs.setoid (hs.some (hs.index x)) x$$$

Lean4

theorem some_index (x : α) : hs.setoid (hs.some (hs.index x)) x :=
  hs.index_some (hs.index x)

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

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

Разделы

Аффилиация

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