equivFinOfCardEq — Mathlib

English

There is a noncomputable equivalence between a finset s and Fin #s.

Русский

Существует невычислимое эквивалентное отображение между конечным множеством s и Fin #s.

LaTeX

$$$s \\equiv Fin\\#s$$$

Lean4

/-- Noncomputable equivalence between a finset `s` as a fintype and `Fin n`, when there is a
proof that `#s = n`. -/
noncomputable def equivFinOfCardEq {s : Finset α} {n : ℕ} (h : #s = n) : s ≃ Fin n :=
  Fintype.equivFinOfCardEq ((Fintype.card_coe _).trans h)

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