fintype — Mathlib

English

If α is finite, then Set α is finite (the collection of all subsets of α is finite).

Русский

Если α конечно, то множество Set α (множество всех подмножеств α) конечно.

LaTeX

$$$\\operatorname{Finite}(\\mathrm{Set}(\\alpha)).$$$

Lean4

instance fintype [Fintype α] : Fintype (Set α) :=
  ⟨(@Finset.univ (Finset α) _).map coeEmb.1, fun s => by
    classical
    refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
    simp⟩
    -- Not to be confused with `Set.Finite`, the predicate

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