ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Bijective map
Set automorphism
Definition D2919
Permutation
Formulation 2
A D353: Set automorphism $f : X \to X$ is a permutation on $X$ if and only if there exists a D11: Set $E$ such that
(1) $E \subseteq X$ is a D78: Subset of $X$
(2) $E$ is a D17: Finite set
(3) $\forall \, x \in X \setminus E : f(x) = x$
Children
D6186: Standard permutation