English
Similarly to previous, the map via insertNthEquiv of the filtered piFinset corresponds to a product of S(p) with the filtered piFinset of (p.removeNth S).
Русский
Аналогично insertNthEquiv: отображение через него переводит отфильтрованное piFinset в произведение S(p) и отфильтрованного piFinset (p.removeNth S).
LaTeX
$$$ \\mathrm{map}(\\mathrm{insertNthEquiv}\\,\\alpha p).symm.toEmbedding \\; {r \\in piFinset S \\\\mid P (p.removeNth r)} = S(p) \\times^{\\!} {r \\in piFinset (p.removeNth S) \\mid P r}$$$
Lean4
theorem map_insertNthEquiv_filter_piFinset (P : (∀ i, α (p.succAbove i)) → Prop) [DecidablePred P] :
{r ∈ piFinset S | P (p.removeNth r)}.map (p.insertNthEquiv α).symm.toEmbedding =
S p ×ˢ {r ∈ piFinset (p.removeNth S) | P r} :=
by unfold removeNth; ext; simp [Fin.forall_iff_succAbove p, and_assoc]
