English
For a predicate P on tail-shape, the filtered piFinset via consEquiv is equal to a product formed by the head and the filtered tail, after transporting through the consEquiv bijection. In symbols, map (consEquiv α) of {r ∈ piFinset S | P (tail r)} equals S(0) × {r ∈ piFinset (tail S) | P r}.
Русский
Для предиката P над хвостовой формой, отображение через consEquiv переводит отфильтрованное piFinset в произведение головы и отфильтрованного хвоста; после транспозиции через биекция consEquiv: map (consEquiv α) {r ∈ piFinset S | P (tail r)} = S(0) × {r ∈ piFinset (tail S) | P r}.
LaTeX
$$$ \\mathrm{map}(\\mathrm{consEquiv}\\,\\alpha).symm\\!\\text{toEmbedding} \\, {r \\in piFinset S \\mid P( tail r )} = S(0) \\times^{\\!} {r \\in piFinset (tail S) \\mid P r}$$$
Lean4
theorem map_consEquiv_filter_piFinset (P : (∀ i, α (succ i)) → Prop) [DecidablePred P] :
{r ∈ piFinset S | P (tail r)}.map (consEquiv α).symm.toEmbedding = S 0 ×ˢ {r ∈ piFinset (tail S) | P r} := by
unfold tail; ext; simp [Fin.forall_iff_succ, and_assoc]
