English
Dual to the cons case, the filtered piFinset via snocEquiv corresponds to a product of the last component and the filtered init, transported by snocEquiv.
Русский
Аналогично случаю cons, для snocEquiv отображение переводит отфильтрованное piFinset в произведение последнего элемента и отфильтрованного init, через snocEquiv.
LaTeX
$$$ \\mathrm{map}(\\mathrm{snocEquiv}\\,\\alpha).symm\\!\\text{toEmbedding} \\; {r \\in piFinset S \\mid P (init r)} = S( last\\,\\_. ) \\times^{\\!} {r \\in piFinset (init S) \\mid P r}$$$
Lean4
theorem map_snocEquiv_filter_piFinset (P : (∀ i, α (castSucc i)) → Prop) [DecidablePred P] :
{r ∈ piFinset S | P (init r)}.map (snocEquiv α).symm.toEmbedding = S (last _) ×ˢ {r ∈ piFinset (init S) | P r} := by
unfold init; ext; simp [Fin.forall_iff_castSucc, and_assoc]
