English
There is a natural equivalence between embeddings Fin(n+1) ↪ ι and a Sigma-type consisting of an embedding Fin n ↪ ι and a value not in the range of that embedding.
Русский
Существуют естественные эквивалентности между вложениями Fin(n+1) ↪ ι и сигма-типом, состоящим из вложения Fin n ↪ ι и значения, не попадающего в область вложения.
LaTeX
$$$$ \\mathrm{embeddingFinSucc}(n, ι) : (\\mathrm{Fin}(n+1) \\hookrightarrow ι) \\simeq \\Sigma (e : \\mathrm{Fin}(n) \\hookrightarrow ι), \\{ i \\mid i \\notin \\mathrm{range}(e) \\}. $$$$
Lean4
/-- An embedding `e : Fin (n+1) ↪ ι` corresponds to an embedding `f : Fin n ↪ ι` (corresponding
the last `n` coordinates of `e`) together with a value not taken by `f` (corresponding to `e 0`). -/
def embeddingFinSucc (n : ℕ) (ι : Type*) : (Fin (n + 1) ↪ ι) ≃ (Σ (e : Fin n ↪ ι), { i // i ∉ Set.range e }) :=
((finSuccEquiv n).embeddingCongr (Equiv.refl ι)).trans (Function.Embedding.optionEmbeddingEquiv (Fin n) ι)
