cycleIcc_def_le — Mathlib

English

If i ≤ j, then the action of cycleIcc i j on k ∈ Fin n equals the lifted cycleRange action on the corresponding element.

Русский

Если i ≤ j, то действие cycleIcc i j на k ∈ Fin n совпадает с действием поднятого cycleRange на соответствующий элемент.

LaTeX

$$$(i \le j) \implies (i.j).cycleIcc(k) = ((j - i).castLT(\text{sub\_val\_lt\_sub}(i\le j))).cycleRange\big(((natAddCastLEEmb (Nat.subLe n i)).toEquivRange)^{-1}(k)\big)$$$

Lean4

@[simp]
theorem cycleIcc_def_le {i j : Fin n} (hij : i ≤ j) :
    cycleIcc i j =
      (cycleRange ((j - i).castLT (sub_val_lt_sub hij))).extendDomain
        (natAdd_castLEEmb (Nat.sub_le n i)).toEquivRange :=
  by simp [cycleIcc, hij]

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