English
Inserting a pivot at position p into an (n+1)-tuple and corresponding inserted sets preserves the piFinset membership: insertNth p x_pivot x_remove ∈ piFinset (insertNth p s_pivot s_remove) iff x_pivot ∈ s_pivot and x_remove ∈ piFinset s_remove.
Русский
При вставке на позицию p элемент x_pivot и соответствующий наборы образуют новый кортеж; членство сохраняется: insertNth p x_pivot x_remove ∈ piFinset (insertNth p s_pivot s_remove) эквивалентно x_pivot ∈ s_pivot и x_remove ∈ piFinset s_remove.
LaTeX
$$$ insertNth\\,p\\,x\\_pivot\\,x\\_remove \\in \\ piFinset (insertNth\\,p\\,s\\_pivot\\,s\\_remove) \\iff x\\_pivot \\in s\\_pivot \\wedge x\\_remove \\in \\ piFinset s\\_remove $$$
Lean4
theorem insertNth_mem_piFinset_insertNth {x_pivot : α p} {x_remove : ∀ i, α (succAbove p i)} {s_pivot : Finset (α p)}
{s_remove : ∀ i, Finset (α (succAbove p i))} :
insertNth p x_pivot x_remove ∈ piFinset (insertNth p s_pivot s_remove) ↔
x_pivot ∈ s_pivot ∧ x_remove ∈ piFinset s_remove :=
by simp [mem_piFinset_iff_pivot_removeNth p]
