finSuccEquiv'_symm_some_below — Mathlib

English

If h : m.castSucc < i, then (finSuccEquiv' i).symm (Some m) = Fin.castSucc m.

Русский

Если h: m.castSucc < i, тогда (finSuccEquiv' i).symm (Some m) = Fin.castSucc m.

LaTeX

$$$(\\mathrm{finSuccEquiv'}\\ i).\\mathrm{symm}\\ (\\mathrm{Some}(m)) = \\mathrm{Fin.castSucc}(m)$$$

Lean4

theorem finSuccEquiv'_symm_some_below {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) :
    (finSuccEquiv' i).symm (some m) = Fin.castSucc m :=
  Fin.succAbove_of_castSucc_lt i m h

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