filter_piFinset_eq_map_consEquiv — Mathlib

English

The filtered piFinset via tail aligns with a consEquiv-based map to the product S(0) × {r ∈ piFinset (tail S) | P r}. The equality is exact.

Русский

Отфильтрованное через tail совпадает с отображением через consEquiv на произведение S(0) × {r ∈ piFinset (tail S) | P r}. Тождество точное.

LaTeX

$$$ {r \\in piFinset S | P (tail r)} = (S 0 \\timesˢ {r \\in piFinset (tail S) | P r}).map (consEquiv α).toEmbedding $$$

Lean4

theorem filter_piFinset_eq_map_consEquiv (P : (∀ i, α (succ i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (tail r)} = (S 0 ×ˢ {r ∈ piFinset (tail S) | P r}).map (consEquiv α).toEmbedding := by
  simp [← map_consEquiv_filter_piFinset, map_map]

Похожие утверждения