filter_piFinset_eq_map_snocEquiv — Mathlib

English

Analogously for snocEquiv, the filtered piFinset via init corresponds to (S(last) × {r ∈ piFinset (init S) | P r}).map (snocEquiv α).

Русский

Аналогично для snocEquiv: отфильтрованное через init соответствует произведению (S(last) × {r ∈ piFinset (init S) | P r}) через отображение snocEquiv.

LaTeX

$$$ {r \\in piFinset S | P (init r)} = (S (last \\, n) \\timesˢ {r \\in piFinset (init S) | P r}).map (snocEquiv α).toEmbedding $$$

Lean4

theorem filter_piFinset_eq_map_snocEquiv (P : (∀ i, α (castSucc i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (init r)} = (S (last _) ×ˢ {r ∈ piFinset (init S) | P r}).map (snocEquiv α).toEmbedding := by
  simp [← map_snocEquiv_filter_piFinset, map_map]

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