toList_getElem_zero

Mathlib.GroupTheory.Perm.Cycle.Concrete

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.toList_getElem_zero

English

If x is in the support of p, then the first element of toList p x is x.

Русский

Если x ∈ поддержка p, то первый элемент toList p x равен x.

LaTeX

$$$$x \in p.\mathrm{support} \Rightarrow (\mathrm{toList}\ p\ x)[0] = x.$$$$

Lean4

theorem toList_getElem_zero (h : x ∈ p.support) : (toList p x)[0]'(length_toList_pos_of_mem_support _ _ h) = x := by
  simp [toList]

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

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

Разделы

Аффилиация

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