lt_finRotate_iff_ne_last — Mathlib

English

For i in Fin(n+1), i < finRotate(n+1) i if and only if i ≠ Fin.last n.

Русский

Для i ∈ Fin(n+1) выполняется: i < finRotate(n+1) i тогда и только тогда, когда i ≠ Fin.last n.

LaTeX

$$$ i < \\mathrm{finRotate}(n+1)\\, i \\\\iff i \\neq \\mathrm{Fin.last}(n) $$$

Lean4

theorem lt_finRotate_iff_ne_last (i : Fin (n + 1)) : i < finRotate _ i ↔ i ≠ Fin.last n :=
  by
  refine ⟨fun hi hc ↦ ?_, fun hi ↦ ?_⟩
  · simp only [hc, finRotate_succ_apply, Fin.last_add_one, Fin.not_lt_zero] at hi
  · rw [Fin.lt_iff_val_lt_val, coe_finRotate_of_ne_last hi, Nat.lt_add_one_iff]

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