inv_left

Mathlib.GroupTheory.Perm.Support

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

English

If f and g are disjoint, then f^{-1} and g are disjoint.

Русский

Если f и g раздельны, то f^{-1} и g раздельны.

LaTeX

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

Lean4

theorem inv_left (h : Disjoint f g) : Disjoint f⁻¹ g := by
  intro x
  rw [inv_eq_iff_eq, eq_comm]
  exact h x

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

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

Разделы

Аффилиация

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