symm

Mathlib.GroupTheory.Perm.Support

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

English

If two permutations are disjoint, then they are disjoint in the opposite order.

Русский

Если две перестановки раздельны, то они раздельны и в обратном порядке.

LaTeX

$$$\operatorname{Disjoint}(f,g) \rightarrow \operatorname{Disjoint}(g,f)$$$

Lean4

@[symm]
theorem symm : Disjoint f g → Disjoint g f := by simp only [Disjoint, or_comm, imp_self]

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

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

Разделы

Аффилиация

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