disjoint_comm

Mathlib.GroupTheory.Perm.Support

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

English

Disjoint is equivalent to the property ∀ x, f(x) = x or g(x) = x.

Русский

Раздельность эквивалентна свойству ∀ x, f(x) = x или g(x) = x.

LaTeX

$$$\operatorname{Disjoint}(f,g) \iff \forall x:\alpha,\ f(x)=x \lor g(x)=x$$$

Lean4

theorem disjoint_comm : Disjoint f g ↔ Disjoint g f :=
  ⟨Disjoint.symm, Disjoint.symm⟩

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

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

Разделы

Аффилиация

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