sign_cycleIcc_of_ge — Mathlib

English

If i ≤ j, then the sign of cycleIcc(j,i) is 1.

Русский

Если i ≤ j, знак cycleIcc(j,i) равен 1.

LaTeX

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

Lean4

theorem sign_cycleIcc_of_ge (hij : i ≤ j) : Perm.sign (cycleIcc j i) = 1 :=
  by
  rcases Fin.lt_or_eq_of_le hij with hij | hij
  · simp [Fin.not_le.mpr hij]
  · rw [hij, sign_cycleIcc_of_eq]

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