filter_piFinset_eq_map_insertNthEquiv

English

The filtered piFinset by p.removeNth over S, after applying insertNthEquiv, equals the sProd of S(p) with the filtered piFinset of (p.removeNth S).

Русский

Отфильтрованное через p.removeNth и применённое insertNthEquiv равно произведению S(p) на отфильтрованное piFinset (p.removeNth S).

LaTeX

$$$ {r \\in piFinset S | P (p.removeNth r)} = (S p \\timesˢ {r \\in piFinset (p.removeNth S) | P r}).map (p.insertNthEquiv α).toEmbedding $$$

Lean4

theorem filter_piFinset_eq_map_insertNthEquiv (P : (∀ i, α (p.succAbove i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (p.removeNth r)} =
      (S p ×ˢ {r ∈ piFinset (p.removeNth S) | P r}).map (p.insertNthEquiv α).toEmbedding :=
  by simp [← map_insertNthEquiv_filter_piFinset, map_map]

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