compositionAsSetEquiv — Mathlib

English

There is a canonical bijection between the set of compositions of n and the Finset of Fin(n−1).

Русский

Существует каноническое биекционное соответствие между множеством композиции числа n и конечным множеством Fin(n−1).

LaTeX

$$$\mathrm{CompositionAsSet}(n) \simeq \mathrm{Finset}(\mathrm{Fin}(n-1))$$$

Lean4

/-- Bijection between compositions of `n` and subsets of `{0, ..., n-2}`, defined by
considering the restriction of the subset to `{1, ..., n-1}` and shifting to the left by one. -/
def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1))
    where
  toFun c := {i : Fin (n - 1) | (⟨1 + (i : ℕ), by omega⟩ : Fin n.succ) ∈ c.boundaries}.toFinset
  invFun
    s :=
    { boundaries :=
        {i : Fin n.succ | i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_hj : j ∈ s), (i : ℕ) = j + 1}.toFinset
      zero_mem := by simp
      getLast_mem := by simp }
  left_inv := by
    intro c
    ext i
    simp only [add_comm, Set.toFinset_setOf, Finset.mem_univ, Finset.mem_filter, true_and, exists_prop]
    constructor
    · rintro (rfl | rfl | ⟨j, hj1, hj2⟩)
      · exact c.zero_mem
      · exact c.getLast_mem
      · convert hj1
    · simp only [or_iff_not_imp_left, ← ne_eq, ← Fin.exists_succ_eq]
      rintro i_mem ⟨j, rfl⟩ i_ne_last
      rcases Nat.exists_add_one_eq.mpr j.pos with ⟨n, rfl⟩
      obtain ⟨k, rfl⟩ : ∃ k : Fin n, k.castSucc = j := by simpa [Fin.exists_castSucc_eq] using i_ne_last
      use k
      simpa using i_mem
  right_inv := by
    intro s
    ext i
    have : (i : ℕ) + 1 ≠ n := by
      apply ne_of_lt
      convert add_lt_add_right i.is_lt 1
      apply (Nat.succ_pred_eq_of_pos _).symm
      exact Nat.lt_of_lt_pred (Fin.pos i)
    simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf, Finset.mem_filter_univ,
      reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff, exists_eq_right']

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