finsetEquivSet — Mathlib

English

There is a natural equivalence between Finset α and Set α when α is finite.

Русский

Существует естественное эквиваленто между Finset α и Set α, если α конечно.

LaTeX

$$$\mathrm{Finset}\;\alpha \simeq \mathrm{Set}\;\alpha$$$

Lean4

/-- Given `Fintype α`, `finsetEquivSet` is the equiv between `Finset α` and `Set α`. (All
sets on a finite type are finite.) -/
noncomputable def finsetEquivSet : Finset α ≃ Set α
    where
  toFun := (↑)
  invFun := by classical exact fun s => s.toFinset
  left_inv s := by convert Finset.toFinset_coe s
  right_inv s := by classical exact s.coe_toFinset

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