finsetSetFinite — Mathlib

English

There is an order isomorphism between Finset α and the subtype { s ⊆ α | s is finite }.

Русский

Существует биекция порядка между Finset α и подтипом {s ⊆ α | s конечен}.

LaTeX

$$$\\text{Finset }\\alpha \\cong_o \\{ s : \\mathcal{P}(\\alpha) \\mid s \\text{ finite} \\}.$$$

Lean4

/-- `Finset α` is order isomorphic to the type of finite sets in `α`. -/
@[simps]
noncomputable def finsetSetFinite : Finset α ≃o { s : Set α // s.Finite }
    where
  toFun s := ⟨s, s.finite_toSet⟩
  invFun s := s.2.toFinset
  left_inv _ := by simp
  right_inv _ := by simp
  map_rel_iff' := .rfl

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