card_snocEquiv_filter_piFinset — Mathlib

English

Analogous to ConsEquiv, the cardinality of the snocEquiv-filtered piFinset equals the product of the last-set cardinality and the init-filtered piFinset cardinality.

Русский

Аналогично ConsEquiv, число элементов через snocEquiv равно произведению размера последнего множества и кардинальности отфильтрованного init.

LaTeX

$$$ {r \\in piFinset S | P (init r)}.card = (S (last _)).card \\cdot {r \\in piFinset (init S) | P r}.card $$$

Lean4

theorem card_snocEquiv_filter_piFinset (P : (∀ i, α (castSucc i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (init r)}.card = (S (last _)).card * {r ∈ piFinset (init S) | P r}.card := by
  rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]

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