English
There exists an injective function on the integers with finite support; i.e., it only moves finitely many integers and fixes the rest.
Русский
Существуют инъективные отображения на целых, которые перемещают только конечное множество целых и остаются тождественными вне него.
LaTeX
$$$\exists f:\mathbb{Z}\to\mathbb{Z},\; \text{Injective}(f) \wedge \#\{n\in\mathbb{Z}: f(n)\neq n\}<\infty$$$
Lean4
instance : Arbitrary (InjectiveFunction ℤ) where
arbitrary := do
let ⟨sz⟩ ← Gen.up Gen.getSize
let xs' := Int.range (-(2 * sz + 2)) (2 * sz + 2)
let ys ← Gen.permutationOf xs'
have Hinj : Injective fun r : ℕ => -(2 * sz + 2 : ℤ) + ↑r := fun _x _y h => Int.ofNat.inj (add_right_injective _ h)
let r : InjectiveFunction ℤ :=
InjectiveFunction.mk.{0} xs' ys.1 ys.2 (ys.2.nodup_iff.1 <| List.nodup_range.map Hinj)
pure r
