English
Let p be a position in Fin(n+1). For a family S and function f with f(i) ∈ S(i), membership of f in the dependent product piFinset S is equivalent to the pivot value f(p) being in S(p) and the function obtained by removing the p-th component, removeNth p f, belonging to piFinset (removeNth p S).
Русский
Пусть p — позиция в Fin(n+1). Пусть S и f задают соответствующие множества и значения. Тогда f ∈ piFinset S эквивалентно f(p) ∈ S(p) и removeNth p f ∈ piFinset (removeNth p S).
LaTeX
$$$ f \\in \\piFinset S \\;\\Longleftrightarrow\\; f(p) \\in S(p) \\wedge removeNth\\,p\\,f \\in \\piFinset (removeNth\\,p\\,S) $$$
Lean4
theorem mem_piFinset_iff_pivot_removeNth (p : Fin (n + 1)) :
f ∈ piFinset s ↔ f p ∈ s p ∧ removeNth p f ∈ piFinset (removeNth p s) := by
simp only [Fintype.mem_piFinset, forall_iff_succAbove p, removeNth]
