cycleRange_of_le — Mathlib

English

For i ≤ j, (cycleRange(j))(i) = 0 if i=j else i+1.

Русский

Для i ≤ j, (cycleRange(j))(i) = 0, если i=j, иначе i+1.

LaTeX

$$$ (\\mathrm{cycleRange}(j))(i) = \\begin{cases}0, & i=j \\\\ i+1, & i

Lean4

theorem cycleRange_of_le [NeZero n] (h : i ≤ j) : cycleRange j i = if i = j then 0 else i + 1 :=
  by
  have iin : i ∈ Set.range (castLEEmb (n := j + 1) (by cutsat)) := by simpa using by cutsat
  have : (castLEEmb (by cutsat)).toEquivRange (castLT i (by cutsat)) = ⟨i, iin⟩ := by
    simpa only [coe_castLEEmb] using by rfl
  rw [cycleRange, (finRotate (j + 1)).extendDomain_apply_subtype (castLEEmb (by cutsat)).toEquivRange iin,
    Function.Embedding.toEquivRange_apply]
  split_ifs with ch
  · have : ((castLEEmb (by cutsat)).toEquivRange.symm ⟨i, iin⟩) = last j := by
      simpa only [coe_castLEEmb, ← this, symm_apply_apply] using eq_of_val_eq (by simp [ch])
    rw [this, finRotate_last]
    rfl
  · have hj1 : (i + 1).1 = i.1 + 1 := val_add_one_of_lt' (by cutsat)
    have hj2 : (i.castLT (by cutsat) + 1 : Fin (j + 1)).1 = (i.castLT (by cutsat) : Fin (j + 1)) + 1 :=
      val_add_one_of_lt' (by simpa using by cutsat)
    exact eq_of_val_eq (by simp [← this, hj1, hj2])

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