Injections into infinite sets of countable indices

An infinite subset of a countable type admits a self-injection that fixes any prescribed finite subset of the target. This lets us reindex a countable sequence or an array axis into an infinite coordinate subset while leaving distinguished coordinates unchanged.

theorem Set.Infinite.exists_injective_into_eqOn_of_finite {ι : Type u_1} [Countable ι] {S F : Set ι} (hS : S.Infinite) (hF : F.Finite) (hFS : F ⊆ S) : ∃ (a : ι → ι), Function.Injective a ∧ (∀ i ∈ F, a i = i) ∧ ∀ (k : ι), a k ∈ S

An injection into an infinite subset of a countable type can fix any prescribed finite subset of its target.