formPerm_apply_of_notMem

Mathlib.GroupTheory.Perm.List

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

English

If x ∉ l, then formPerm(l) x = x.

Русский

Если x ∉ l, то formPerm(l) x = x.

LaTeX

$$$x \\notin l \\Rightarrow \\operatorname{formPerm}(l) x = x$$$

Lean4

theorem formPerm_apply_of_notMem (h : x ∉ l) : formPerm l x = x :=
  not_imp_comm.1 mem_of_formPerm_apply_ne h

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

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

Разделы

Аффилиация

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