coe_notMemRangeEquiv_symm — Mathlib

English

Let k ∈ ℕ. The inverse of the natural equivalence between ℕ and the set {n ∈ ℕ | n ∉ range(k)} is given by j ↦ j + k; more precisely, ((notMemRangeEquiv k).symm)(j) = ⟨j + k, j + k ∉ range(k)⟩ for all j ∈ ℕ.

Русский

Пусть k ∈ ℕ. Обратное отображение биекции между ℕ и множеством {n ∈ ℕ | n ∉ range(k)} задаётся отображением j ↦ j + k; то есть для каждого j ∈ ℕ имеет место ⟨j + k, j + k ∉ range(k)⟩.

LaTeX

$$$ ((\\mathrm{notMemRangeEquiv}(k))^{-1})(j) = \\langle j+k, j+k \\notin \\operatorname{range}(k)\\rangle. $$$

Lean4

@[simp]
theorem coe_notMemRangeEquiv_symm (k : ℕ) :
    ((notMemRangeEquiv k).symm : ℕ → { n // n ∉ range k }) = fun j => ⟨j + k, by simp⟩ :=
  rfl

Похожие утверждения