coe_embeddingFinSucc_symm — Mathlib

English

The inverse of embeddingFinSucc, when viewed as a function, maps f to Fin.cons(f.2.1, f.1).

Русский

Обратное вложение embeddingFinSucc, рассматриваемое как функция, отображает f в Fin.cons(f.2.1, f.1).

LaTeX

$$$$ ((\\mathrm{Equiv.embeddingFinSucc}\\ n\\ ι).symm\\ f) : \\mathrm{Fin}(n+1) \\to ι = \\mathrm{Fin.cons}(f.2.1, f.1). $$$$

Lean4

@[simp]
theorem coe_embeddingFinSucc_symm {n : ℕ} {ι : Type*} (f : Σ (e : Fin n ↪ ι), { i // i ∉ Set.range e }) :
    ((Equiv.embeddingFinSucc n ι).symm f : Fin (n + 1) → ι) = Fin.cons f.2.1 f.1 :=
  by
  ext i
  exact Fin.cases rfl (fun j ↦ rfl) i

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