mem_iff_index_eq

Mathlib.Data.Setoid.Partition

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

English

x ∈ s_i if and only if index x equals i.

Русский

x принадлежит s_i тогда, когда индекс x равен i.

LaTeX

$$$x \\in s_i \\iff hs.index x = i$$$

Lean4

theorem mem_iff_index_eq {x i} : x ∈ s i ↔ hs.index x = i :=
  ⟨fun hxi => (hs.eq_of_mem hxi (hs.mem_index x)).symm, fun h => h ▸ hs.mem_index _⟩

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

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

Разделы

Аффилиация

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