card_insertNthEquiv_filter_piFinset

English

The cardinality of the piFinset after insertNthEquiv equals the product of the involved cardinalities at position p and the rest.

Русский

Число элементов после вставки через insertNthEquiv равно произведению размеров соответствующей головы и хвоста.

LaTeX

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

Lean4

theorem card_insertNthEquiv_filter_piFinset (P : (∀ i, α (p.succAbove i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (p.removeNth r)}.card = (S p).card * {r ∈ piFinset (p.removeNth S) | P r}.card := by
  rw [← card_product, ← map_insertNthEquiv_filter_piFinset, card_map]

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