English
Consider cons x_zero x_tail constructing a (n+1)-tuple from its head and tail. An element of the piFinset over the cons of s_zero and s_tail is equivalent to x_zero ∈ s_zero and x_tail ∈ piFinset s_tail.
Русский
Для конструирования (n+1)-кортежа через head и tail членство элемента в piFinset конуса эквивалентно x_zero ∈ s_zero и x_tail ∈ piFinset s_tail.
LaTeX
$$$ cons\\,x\\_zero\\,x\\_tail \\in \\ piFinset (cons\\,s\\_zero\\,s\\_tail) \\iff x\\_zero \\in s\\_zero \\wedge x\\_tail \\in \\ piFinset s\\_tail $$$
Lean4
theorem cons_mem_piFinset_cons {x_zero : α 0} {x_tail : (i : Fin n) → α i.succ} {s_zero : Finset (α 0)}
{s_tail : (i : Fin n) → Finset (α i.succ)} :
cons x_zero x_tail ∈ piFinset (cons s_zero s_tail) ↔ x_zero ∈ s_zero ∧ x_tail ∈ piFinset s_tail := by
simp_rw [mem_piFinset_iff_zero_tail, cons_zero, tail_cons]
