English
Let S be a family of finite sets S(i) indexed by i in Fin(n+1) and let f be a dependent function with f(i) ∈ S(i) for all i. Then f is in the dependent finite product piFinset S iff its first coordinate lies in S(0) and the tail of f (the restriction to indices i.succ) lies in piFinset (tail S).
Русский
Пусть S задаёт конечные множества S(i) для i ∈ Fin(n+1) и пусть f — зависимая функция с f(i) ∈ S(i) для всех i. Тогда f принадлежит произведению piFinset S тогда, когда f(0) ∈ S(0) и хвост функции tail(f) принадлежит piFinset (tail S).
LaTeX
$$$ f \\in \\piFinset S \\;\\Longleftrightarrow\\; f(0) \\in S(0) \\wedge tail(f) \\in \\piFinset (tail\\,S) $$$
Lean4
theorem mem_piFinset_iff_zero_tail : f ∈ Fintype.piFinset s ↔ f 0 ∈ s 0 ∧ tail f ∈ piFinset (tail s) := by
simp only [Fintype.mem_piFinset, forall_fin_succ, tail]
