cycleIcc_ge — Mathlib

English

If i ≤ j then the cycle from j to i is the identity.

Русский

Если i ≤ j, то цикл cycleIcc(j,i) является тождественным.

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i,j : \\mathrm{Fin}(n)},\\; i \\le j \\Rightarrow \\mathrm{cycleIcc}(j,i) = 1$$$

Lean4

@[simp]
theorem cycleIcc_ge (hij : i ≤ j) [NeZero n] : cycleIcc j i = 1 :=
  by
  rcases Fin.lt_or_eq_of_le hij with hij | hij
  · simp [hij]
  · rw [hij, ← cycleIcc_eq]

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