feat(data/set/countable): finite sets are countable

Author: johoelzl

data/encodable.lean

@@ -20,19 +20,15 @@ variables {α : Type*} {β : Type*}
 
 open encodable
 
-/-
-
-def encodable_finType* [instance] {α : Type*} [h₁ : finType* α] [h₂ : decidable_eq α] :
-  encodable α :=
-encodable.mk
-  (λ a, find a (elements_of α))
-  (λ n, nth (elements_of α) n)
-  (λ a, find_nth (finType*.complete a))
--/
-
 instance encodable_nat : encodable nat :=
 encodable.mk (λ a, a) (λ n, some n) (λ a, rfl)
 
+instance encodable_empty : encodable empty :=
+encodable.mk (λ a:_root_.empty, a.rec _) (λ n, none) (λ a:_root_.empty, a.rec _)
+
+instance encodable_unit : encodable unit :=
+encodable.mk (λ_, 0) (λn, if n = 0 then some () else none) (λ⟨⟩, by simp)
+
 instance encodable_option {α : Type*} [h : encodable α] : encodable (option α) :=
 encodable.mk
   (λ o, match o with
@@ -320,6 +316,8 @@ def encodable_of_equiv [h : encodable α] : α ≃ β → encodable β
     (λ b, by rewrite r; reflexivity)
 end
 
+instance : encodable bool := encodable_of_equiv equiv.bool_equiv_unit_sum_unit.symm
+
 end encodable
 
 /-

data/set/countable.lean

@@ -102,4 +102,25 @@ by_cases
         ⟨nat.mkpair i j, by simp [function.comp, nat.unpair_mkpair, hi, hj]⟩⟩)
   (assume : ¬ nonempty α, ⟨λ_, 0, assume a, (this ⟨a⟩).elim⟩)
 
+lemma countable_Union {s : set α} {t : α → set β} (hs : countable s) (ht : ∀a∈s, countable (t a)) :
+  countable (⋃a∈s, t a) :=
+have ⋃₀ (t '' s) = (⋃a∈s, t a), from lattice.Sup_image,
+by rw [←this];
+from (countable_sUnion (countable_image hs) $ assume a ⟨s', hs', eq⟩, eq ▸ ht s' hs')
+
+lemma countable_union {s₁ s₂ : set α} (h₁ : countable s₁) (h₂ : countable s₂) : countable (s₁ ∪ s₂) :=
+have s₁ ∪ s₂ = (⨆b ∈ ({tt, ff} : set bool), bool.cases_on b s₁ s₂),
+  by simp [lattice.supr_or, lattice.supr_sup_eq]; refl,
+by rw [this]; from countable_Union countable_encodable (assume b,
+  match b with
+  | tt := by simp [h₂]
+  | ff := by simp [h₁]
+  end)
+
+lemma countable_insert {s : set α} {a : α} (h : countable s) : countable (insert a s) :=
+by rw [set.insert_eq]; from countable_union countable_singleton h
+
+lemma countable_finite {s : set α} (h : finite s) : countable s :=
+h.rec_on countable_empty $ assume a s _ _, countable_insert
+
 end set