card_derangements_fin_add_two — Mathlib

English

For every natural n, the number of derangements on Fin(n+2) satisfies D(n+2) = (n+1)[D(n) + D(n+1)], where D(k) denotes the number of derangements of Fin(k).

Русский

Для каждого натурального n верно, что число перестановок без фиксированных точек на Fin(n+2) удовлетворяет рекуррентному закону D(n+2) = (n+1)[D(n) + D(n+1)], где D(k) — число таких перестановок на Fin(k).

LaTeX

$$$\\#\\mathrm{derangements}(\\mathrm{Fin}(n+2)) = (n+1)\\#\\mathrm{derangements}(\\mathrm{Fin}(n)) + (n+1)\\#\\mathrm{derangements}(\\mathrm{Fin}(n+1)).$$$

Lean4

theorem card_derangements_fin_add_two (n : ℕ) :
    card (derangements (Fin (n + 2))) =
      (n + 1) * card (derangements (Fin n)) + (n + 1) * card (derangements (Fin (n + 1))) :=
  by
  -- get some basic results about the size of Fin (n+1) plus or minus an element

  have h1 : ∀ a : Fin (n + 1), card ({ a }ᶜ : Set (Fin (n + 1))) = card (Fin n) :=
    by
    intro a
    simp only [card_ofFinset (s := Finset.filter (fun x => x ∈ ({ a }ᶜ : Set (Fin (n + 1)))) Finset.univ),
      Set.mem_compl_singleton_iff, Finset.filter_ne' _ a, Finset.card_erase_of_mem (Finset.mem_univ a), Finset.card_fin,
      add_tsub_cancel_right, card_fin]
  have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by
    simp only [card_fin, card_option]
      -- rewrite the LHS and substitute in our fintype-level equivalence

  simp only [card_derangements_invariant h2, card_congr (@derangementsRecursionEquiv (Fin (n + 1)) _),
    -- push the cardinality through the Σ and ⊕ so that we can use `card_n`
    card_sigma, card_sum, card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin, mul_add,
    Nat.cast_id]

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