finSuccEquiv'_below

Mathlib.Logic.Equiv.Fin.Basic

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

← MathLib Explorer

English

If m.castSucc < i, then (finSuccEquiv' i)(m.castSucc) = m.

Русский

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

LaTeX

$$$\\text{If } m.\\mathrm{castSucc} < i,\\; (\\mathrm{finSuccEquiv'}\\ i)(m.\\mathrm{castSucc}) = m$$$

Lean4

theorem finSuccEquiv'_below {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) :
    (finSuccEquiv' i) (Fin.castSucc m) = m := by rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]

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

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

Разделы

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

Аффилиация

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