finSuccEquiv'_symm_coe_below

Mathlib.Logic.Equiv.Fin.Basic

URI: https://scilib.ai/kg/mathlib#finSuccEquiv'_symm_coe_below

← MathLib Explorer

English

If h: m.castSucc < i, then (finSuccEquiv' i).symm (Option.some m) equals m.castSucc.

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru