mul_right

Mathlib.GroupTheory.Perm.Support

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

English

If Disjoint f g and Disjoint f h, then Disjoint f (g h).

Русский

Если Disjoint f g и Disjoint f h, то Disjoint f (g h).

LaTeX

$$$\operatorname{Disjoint}(f,g) \land \operatorname{Disjoint}(f,h) \Rightarrow \operatorname{Disjoint}(f \,(g \cdot h))$$$

Lean4

theorem mul_right (H1 : Disjoint f g) (H2 : Disjoint f h) : Disjoint f (g * h) :=
  by
  rw [disjoint_comm]
  exact H1.symm.mul_left H2.symm

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

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

Разделы

Аффилиация

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