mem_of_formPerm_apply_ne

Mathlib.GroupTheory.Perm.List

URI: https://scilib.ai/kg/mathlib#List.mem_of_formPerm_apply_ne

← MathLib Explorer

English

If l.formPerm x ≠ x, then x ∈ l.

Русский

Если l.formPerm x ≠ x, то x ∈ l.

LaTeX

$$$\\operatorname{formPerm}(l)\\,x \\neq x \\Rightarrow x \\in l$$$

Lean4

theorem mem_of_formPerm_apply_ne (h : l.formPerm x ≠ x) : x ∈ l := by
  simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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