English
Let S be a family of finite sets indexed by Fin(n+1) and f a dependent function with f(i) ∈ S(i). Then f ∈ piFinset S if and only if its last value f(last n) lies in S(last n) and the initial segment init f lies in piFinset (init S).
Русский
Пусть S задаёт конечные множества S(i) для i ∈ Fin(n+1) и пусть f — зависимая функция с f(i) ∈ S(i). Тогда f принадлежит piFinset S тогда, когда f(правая граница) ∈ S(правая граница) и начальная часть init f принадлежит piFinset (init S).
LaTeX
$$$ f \\in \\piFinset S \\;\\Longleftrightarrow\\; f(\\text{last } n) \\in S(\\text{last } n) \\wedge init(f) \\in \\piFinset (init\\,S) $$$
Lean4
theorem mem_piFinset_iff_last_init : f ∈ piFinset s ↔ f (last n) ∈ s (last n) ∧ init f ∈ piFinset (init s) := by
simp only [Fintype.mem_piFinset, forall_fin_succ', init, and_comm]
