Extending a finite injection into ℕ to a permutation

A small graph-independent lemma, reused by both the graph exchangeability API (Graphon.InfiniteGraph.exists_perm_extend) and the generic relational one (AHK R2c). A candidate for upstreaming to Mathlib.

theorem exists_perm_extend {k : ℕ} (g : Fin k ↪ ℕ) : ∃ (σ : Equiv.Perm ℕ), ∀ (a : Fin k), σ ↑a = g a

Every injection Fin k ↪ ℕ extends to a permutation of ℕ: the ranges are finite so their complements are countably infinite, hence equivalent, and Equiv.Set.compl assembles the permutation.

theorem exists_perm_extend_of_injOn {A : Finset ℕ} {g : ℕ → ℕ} (hg : Set.InjOn g ↑A) : ∃ (σ : Equiv.Perm ℕ), ∀ a ∈ A, σ a = g a

Every finite partial injection of ℕ extends to a permutation: the domain and its image are finite, so their complements are countably infinite and hence equivalent, and Equiv.Set.compl assembles the permutation. Generalizes exists_perm_extend from an initial segment to an arbitrary finite domain.