English
If α is denumerable, then Finset α is also denumerable.
Русский
Если α денумерабельно, то и Finset α денумерабельно.
LaTeX
$$$\operatorname{Denumerable}(\operatorname{Finset} \alpha)$$$
Lean4
/-- If `α` is denumerable, then so is `Finset α`. Warning: this is *not* the same encoding as used
in `Finset.encodable`. -/
instance finset : Denumerable (Finset α) :=
mk'
⟨fun s : Finset α => encode <| lower' ((s.map (eqv α).toEmbedding).sort (· ≤ ·)) 0, fun n =>
Finset.map (eqv α).symm.toEmbedding (raise'Finset (ofNat (List ℕ) n) 0), fun s =>
Finset.eq_of_veq <| by
simp [-Multiset.map_coe, raise'Finset, raise_lower' (fun n _ => Nat.zero_le n) (Finset.sort_sorted_lt _)],
fun n => by
simp [-Multiset.map_coe, Finset.map, raise'Finset, Finset.sort,
List.mergeSort_eq_self _ (raise'_sorted _ _).le_of_lt, lower_raise']⟩
