cycleIcc_zero_eq_cycleRange — Mathlib

English

For i ∈ Fin(n) and n ≠ 0, cycleIcc(0,i) equals cycleRange(i).

Русский

Для i ∈ Fin(n) и n ≠ 0, cycleIcc(0,i) равно cycleRange(i).

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i : \\mathrm{Fin}(n)},\\; n \\neq 0 \\Rightarrow \\mathrm{cycleIcc}(0,i) = \\mathrm{cycleRange}(i)$$$

Lean4

theorem cycleIcc_zero_eq_cycleRange (i : Fin n) [NeZero n] : cycleIcc 0 i = cycleRange i :=
  by
  ext x
  rcases lt_trichotomy x i with ch | ch | ch
  · simp [-cycleIcc_def_le, cycleIcc_of_ge_of_lt (zero_le x) ch, cycleRange_of_lt ch]
  · simp [-cycleIcc_def_le, ch]
  · simp [-cycleIcc_def_le, cycleIcc_of_gt ch, cycleRange_of_gt ch]

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