English
This definition constructs an element of the trajectory space by starting with a fixed initial segment and recursively applying an induction rule to extend the sequence, while maintaining well-foundedness of the construction.
Русский
Это определение строит элемент пространства траекторий, начиная с фиксированного начального сегмента и рекурсивно применяя правило индукции для расширения последовательности, сохраняя базовую корректность.
LaTeX
$$$ \text{iterateInduction}\;{X}\;{a}\;(x)(ind) : \Pi n, X n$$$
Lean4
theorem frestrictLe_iterateInduction {a : ℕ} (x : Π i : Iic a, X i) (ind : (n : ℕ) → (Π i : Iic n, X i) → X (n + 1)) :
frestrictLe a (iterateInduction x ind) = x := by
ext i
simp only [frestrictLe_apply]
obtain ⟨(zero | j), hj⟩ := i <;> rw [iterateInduction]
rw [dif_pos (mem_Iic.1 hj)]
