English
For each k, there is an equivalence between the set of natural numbers not in range k and ℕ, given by n ↦ n − k with inverse m ↦ m + k.
Русский
Для каждого k существует биекция между множеством натуральных чисел, не принадлежащих range(k), и ℕ, задаваемая n ↦ n − k и обратной связью m ↦ m + k.
LaTeX
$$$$ \text{NotMemRangeEquiv}(k) : \{ n \mid n \notin \operatorname{range}(k) \} \simeq \mathbb{N}, \quad n \mapsto n - k, \quad m \mapsto m + k. $$$$
Lean4
/-- Equivalence between the set of natural numbers which are `≥ k` and `ℕ`, given by `n → n - k`. -/
def notMemRangeEquiv (k : ℕ) : { n // n ∉ range k } ≃ ℕ
where
toFun i := i.1 - k
invFun j := ⟨j + k, by simp⟩
left_inv := by grind
right_inv := by grind
