disjoint_iff_eq_or_eq

Mathlib.GroupTheory.Perm.Support

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

English

Disjoint f g holds exactly when for every x, f(x) = x or g(x) = x.

Русский

Раздельность f и g эквивалентна тому, что для каждого 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_iff_eq_or_eq : Disjoint f g ↔ ∀ x : α, f x = x ∨ g x = x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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