disjoint_inv_right_iff

Mathlib.GroupTheory.Perm.Support

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

English

Disjoint f g^{-1} iff Disjoint f g.

Русский

Раздельность f g^{-1} эквивалентна раздельности f g.

LaTeX

$$$\operatorname{Disjoint}(f, g^{-1}) \iff \operatorname{Disjoint}(f,g)$$$

Lean4

@[simp]
theorem disjoint_inv_right_iff : Disjoint f g⁻¹ ↔ Disjoint f g := by
  rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]

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

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

Разделы

Аффилиация

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