English
Let α be a type with finite cardinal. There exists an order isomorphism between Finset α and Set α, i.e., the lattice of finite subsets of α is order-isomorphic to the lattice of all subsets of α, preserving inclusion.
Русский
Пусть α — конечного размера тип. Существует порядковый изоморфизм между Finset α и Set α: множество конечных подмножеств α упорядован по включению эквивалентно всем подмножествам α.
LaTeX
$$$Finset\ α \cong_o Set\ α$$$
Lean4
/-- Given a fintype `α`, `finsetOrderIsoSet` is the order isomorphism between `Finset α` and `Set α`
(all sets on a finite type are finite). -/
@[simps toEquiv]
noncomputable def finsetOrderIsoSet : Finset α ≃o Set α
where
toEquiv := finsetEquivSet
map_rel_iff' := Finset.coe_subset
