coe_cycleRange_of_le — Mathlib

English

If i = j, then (cycleRange j i) = 0.

Русский

Если i = j, то (cycleRange(j,i)) = 0.

LaTeX

$$$ (\\mathrm{cycleRange}(j))(i) = 0 \\quad\\text{если } i=j$$$

Lean4

theorem coe_cycleRange_of_le (h : i ≤ j) : (cycleRange j i : ℕ) = if i = j then 0 else (i : ℕ) + 1 :=
  by
  rcases n with - | n
  · exact absurd le_rfl j.pos.not_ge
  rw [cycleRange_of_le h]
  split_ifs with h'
  · rfl
  exact
    val_add_one_of_lt
      (calc
        (i : ℕ) < j := Fin.lt_iff_val_lt_val.mp (lt_of_le_of_ne h h')
        _ ≤ n := Nat.lt_succ_iff.mp j.2)

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