equivFin — Mathlib

English

There is a natural equivalence between a finset s viewed as a finite type and Fin #s.

Русский

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

LaTeX

$$$s \\text{ как тип эквивалентен } Fin\\#s$$$

Lean4

/-- Noncomputable equivalence between a finset `s` coerced to a type and `Fin #s`. -/
noncomputable def equivFin (s : Finset α) : s ≃ Fin #s :=
  Fintype.equivFinOfCardEq (Fintype.card_coe _)

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