Disjoint — Mathlib

English

Let f and g be permutations of α. They are disjoint if every element is fixed by at least one of them; i.e., for every x in α, either f(x) = x or g(x) = x.

Русский

Пусть f и g — перестановки множества α. Они раздельны, если каждое элемент фиксируется как f, так и g: для любого x ∈ α выполняется f(x) = x или g(x) = x.

LaTeX

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

Lean4

/-- Two permutations `f` and `g` are `Disjoint` if their supports are disjoint, i.e.,
every element is fixed either by `f`, or by `g`. -/
def Disjoint (f g : Perm α) :=
  ∀ x, f x = x ∨ g x = x

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