card_consEquiv_filter_piFinset — Mathlib

English

The cardinality of the filtered piFinset under tail equals the product of the cardinalities of the head set and the tail-filtered piFinset.

Русский

Число элементов отфильтрованного piFinset через tail равно произведению чисел элементов головы и хвоста.

LaTeX

$$$ {r \\in piFinset S | P (tail r)}.card = (S 0).card \\cdot {r \\in piFinset (tail S) | P r}.card $$$

Lean4

theorem card_consEquiv_filter_piFinset (P : (∀ i, α (succ i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (tail r)}.card = (S 0).card * {r ∈ piFinset (tail S) | P r}.card := by
  rw [← card_product, ← map_consEquiv_filter_piFinset, card_map]

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