index_some

Mathlib.Data.Setoid.Partition

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

English

The index of the representative of i is i: index(some i) = i.

Русский

Индекс представителя некоторого i равен i: index(some i) = i.

LaTeX

$$@[simp] theorem index_some (i) : hs.index (hs.some i) = i$$

Lean4

@[simp]
theorem index_some (i : ι) : hs.index (hs.some i) = i :=
  (mem_iff_index_eq _).1 <| hs.some_mem i

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

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

Разделы

Аффилиация

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