mul_left

Mathlib.GroupTheory.Perm.Support

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_left (H1 : Disjoint f h) (H2 : Disjoint g h) : Disjoint (f * g) h := fun x => by
  cases H1 x <;> cases H2 x <;> simp [*]

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

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

Разделы

Аффилиация

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