Order automorphism (source code)

= Order automorphism
{title2=$\operatorname{Aut}(I,<)$}

An <order automorphism> of a <total order> $(I,<)$ is a <bijection> $\pi:I\to I$ such that $i<j$ if and only if $\pi(i)<\pi(j)$. Composition and inverses are again <order automorphisms>. Transporting the indices of an <order-indiscernible sequence> by such a map preserves every <first-order formula> on increasing finite tuples.