support_one

Mathlib.GroupTheory.Perm.Support

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

English

The identity permutation fixes every point, hence its support is empty.

Русский

Единичная перестановка фиксирует каждую точку, поэтому ее опора пустая.

LaTeX

$$$ (1 : \operatorname{Perm} \alpha).\operatorname{support} = \varnothing $$$

Lean4

@[simp]
theorem support_one : (1 : Perm α).support = ∅ := by rw [support_eq_empty_iff]

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

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

Разделы

Аффилиация

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