English
The map frestrictLe applied to iterateInduction x ind equals x. This shows that the iterative construction respects the restriction to the left endpoints.
Русский
Отображение frestrictLe, примененное к iterateInduction x ind, равно x. Это показывает, что итеративная конструкция сохраняет ограничение по левым концам.
LaTeX
$$$ frestrictLe\ a\ (iterateInduction\ x\ ind) = x $$$
Lean4
/-- This function takes as input a tuple `(x_₀, ..., x_ₐ)` and `ind` a function which
given `(y_₀, ...,y_ₙ)` outputs `x_{n+1} : X (n + 1)`, and it builds an element of `Π n, X n`
by starting with `(x_₀, ..., x_ₐ)` and then iterating `ind`. -/
def iterateInduction {a : ℕ} (x : Π i : Iic a, X i) (ind : (n : ℕ) → (Π i : Iic n, X i) → X (n + 1)) : Π n, X n
| 0 => x ⟨0, mem_Iic.2 <| zero_le a⟩
| k + 1 => if h : k + 1 ≤ a then x ⟨k + 1, mem_Iic.2 h⟩ else ind k (fun i ↦ iterateInduction x ind i)
decreasing_by exact Nat.lt_succ.2 (mem_Iic.1 i.2)
