finRotate_of_lt

Mathlib.Logic.Equiv.Fin.Rotate

URI: https://scilib.ai/kg/mathlib#finRotate_of_lt

← MathLib Explorer

English

If k < n, then finRotate(n+1)⟨k,h⟩ = ⟨k+1, Nat.succ_lt_succ h⟩.

Русский

Если k < n, то finRotate(n+1) ⟨k,h⟩ = ⟨k+1, Nat.succ_lt_succ h⟩.

LaTeX

$$$\\forall k\\in\\mathbb{N},\\; h:k

Lean4

theorem finRotate_of_lt {k : ℕ} (h : k < n) :
    finRotate (n + 1) ⟨k, h.trans_le n.le_succ⟩ = ⟨k + 1, Nat.succ_lt_succ h⟩ :=
  by
  ext
  dsimp [finRotate_succ]
  simp [finAddFlip_apply_mk_left h, Nat.add_comm]

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

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

Разделы

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

Аффилиация

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