apply_mem_support

Mathlib.GroupTheory.Perm.Support

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

English

For any permutation f and any x, f(x) belongs to the support of f if and only if x belongs to the support of f.

Русский

Для перестановки f и любого x верно: f(x) ∈ supp(f) ↔ x ∈ supp(f).

LaTeX

$$$f(x) \in \operatorname{supp}(f) \iff x \in \operatorname{supp}(f).$$$

Lean4

theorem apply_mem_support {x : α} : f x ∈ f.support ↔ x ∈ f.support := by
  rw [mem_support, mem_support, Ne, Ne, apply_eq_iff_eq]

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

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

Разделы

Аффилиация

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