English
When i ≤ j, cycleIcc i j is equal to a lifted cycleRange of (j-i) with a domain extension.
Русский
При i ≤ j, cycleIcc i j равен поднятому cycleRange на (j-i) с расширением области определения.
LaTeX
$$cycleIcc i j = (cycleRange ((j - i).castLT (sub_val_lt_sub hij))).extendDomain (natAdd_castLEEmb (Nat.sub_le n i)).toEquivRange$$
Lean4
theorem cycleIcc_to_cycleRange (hij : i ≤ j) (kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i))) :
(cycleIcc i j) k =
(natAdd_castLEEmb (Nat.sub_le n i))
(((j - i).castLT (sub_val_lt_sub hij)).cycleRange
((natAdd_castLEEmb (Nat.sub_le n i)).toEquivRange.symm ⟨k, kin⟩)) :=
by
simp [hij,
((j - i).castLT (sub_val_lt_sub hij)).cycleRange.extendDomain_apply_subtype (natAdd_castLEEmb _).toEquivRange kin]
