conj

Mathlib.GroupTheory.Perm.Support

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

English

If Disjoint f g, then Disjoint (h f h^{-1}) (h g h^{-1}) for any h.

Русский

Если Disjoint f g, то Disjoint (h f h^{-1}) (h g h^{-1}) при любом h.

LaTeX

$$$\forall h:\operatorname{Perm}(\alpha),\ \operatorname{Disjoint}(f,g) \Rightarrow \operatorname{Disjoint}(h f h^{-1}, h g h^{-1})$$$

Lean4

theorem conj (H : Disjoint f g) (h : Perm α) : Disjoint (h * f * h⁻¹) (h * g * h⁻¹) :=
  (disjoint_conj h).2 H

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

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

Разделы

Аффилиация

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