finSuccEquiv'_symm_coe_above — Mathlib

English

Let i be an element of Fin(n+1) and m an element of Fin n with i ≤ castSucc(m). Then the inverse of finSuccEquiv' at i, applied to m, equals m.succ.

Русский

Пусть i ∈ Fin(n+1) и m ∈ Fin(n) удовлетворяют i ≤ castSucc(m). Тогда обратный образ (symm) функции finSuccEquiv' при i, применённый к m, равен m.succ.

LaTeX

$$$$ i \\in \\mathrm{Fin}(n+1) ,\\ m \\in \\mathrm{Fin}(n),\\ i \\leq \\mathrm{Fin.castSucc}(m) \\Rightarrow (\\mathrm{finSuccEquiv}' i)^{-1}(m) = m.succ $$$$

Lean4

theorem finSuccEquiv'_symm_coe_above {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) :
    (finSuccEquiv' i).symm m = m.succ :=
  finSuccEquiv'_symm_some_above h

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