coe_finRotate_of_ne_last — Mathlib

English

If i ∈ Fin (n+1) and i ≠ Fin.last n, then (finRotate(n+1) i : ℕ) = i + 1.

Русский

Если i ∈ Fin(n+1) и i ≠ Fin.last n, то (finRotate(n+1) i) : ℕ = i + 1.

LaTeX

$$$ (\\mathrm{finRotate}(n+1)\\, i : \\mathbb{N}) = i + 1 \\quad \\text{whenever } i \\neq \\mathrm{Fin.last}(n)$$$

Lean4

theorem coe_finRotate_of_ne_last {i : Fin n.succ} (h : i ≠ Fin.last n) : (finRotate (n + 1) i : ℕ) = i + 1 :=
  by
  rw [finRotate_succ_apply]
  have : (i : ℕ) < n := Fin.val_lt_last h
  exact Fin.val_add_one_of_lt this

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