feat(analysis/special_functions/complex/log): exp ⁻¹' s is countable (

#9410)

Also prove that the preimage of a countable set under an injective map
is countable.

src/analysis/special_functions/complex/log.lean

@@ -36,7 +36,7 @@ by rw [log, exp_add_mul_I, ← of_real_sin, sin_arg, ← of_real_cos, cos_arg hx
   mul_div_cancel' _ (of_real_ne_zero.2 (mt abs_eq_zero.1 hx)), ← mul_assoc,
   mul_div_cancel' _ (of_real_ne_zero.2 (mt abs_eq_zero.1 hx)), re_add_im]
 
-lemma range_exp : range exp = {x | x ≠ 0} :=
+@[simp] lemma range_exp : range exp = {0}ᶜ :=
 set.ext $ λ x, ⟨by { rintro ⟨x, rfl⟩, exact exp_ne_zero x }, λ hx, ⟨log x, exp_log hx⟩⟩
 
 lemma exp_inj_of_neg_pi_lt_of_le_pi {x y : ℂ} (hx₁ : -π < x.im) (hx₂ : x.im ≤ π)
@@ -118,6 +118,22 @@ by rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
 lemma exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ n : ℤ, x = y + n * ((2 * π) * I) :=
 by simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']
 
+@[simp] lemma countable_preimage_exp {s : set ℂ} : countable (exp ⁻¹' s) ↔ countable s :=
+begin
+  refine ⟨λ hs, _, λ hs, _⟩,
+  { refine ((hs.image exp).insert 0).mono _,
+    rw [image_preimage_eq_inter_range, range_exp, ← diff_eq, ← union_singleton, diff_union_self],
+    exact subset_union_left _ _ },
+  { rw ← bUnion_preimage_singleton,
+    refine hs.bUnion (λ z hz, _),
+    rcases em (∃ w, exp w = z) with ⟨w, rfl⟩|hne,
+    { simp only [preimage, mem_singleton_iff, exp_eq_exp_iff_exists_int, set_of_exists],
+      exact countable_Union (λ m, countable_singleton _) },
+    { push_neg at hne, simp [preimage, hne] } }
+end
+
+alias countable_preimage_exp ↔ _ set.countable.preimage_cexp
+
 /-- `complex.exp` as a `local_homeomorph` with `source = {z | -π < im z < π}` and
 `target = {z | 0 < re z} ∪ {z | im z ≠ 0}`. This definition is used to prove that `complex.log`
 is complex differentiable at all points but the negative real semi-axis. -/

src/data/set/countable.lean

@@ -102,13 +102,26 @@ lemma countable.mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) : countable s₂ 
 | ⟨H⟩ := ⟨@of_inj _ _ H _ (embedding_of_subset _ _ h).2⟩
 
 lemma countable.image {s : set α} (hs : countable s) (f : α → β) : countable (f '' s) :=
-let f' : s → f '' s := λ⟨a, ha⟩, ⟨f a, mem_image_of_mem f ha⟩ in
-have hf' : surjective f', from assume ⟨b, a, ha, hab⟩, ⟨⟨a, ha⟩, subtype.eq hab⟩,
-⟨@encodable.of_inj _ _ hs.to_encodable (surj_inv hf') (injective_surj_inv hf')⟩
+have surjective ((maps_to_image f s).restrict _ _ _), from surjective_maps_to_image_restrict f s,
+⟨@encodable.of_inj _ _ hs.to_encodable (surj_inv this) (injective_surj_inv this)⟩
 
 lemma countable_range [encodable α] (f : α → β) : countable (range f) :=
 by rw ← image_univ; exact (countable_encodable _).image _
 
+lemma maps_to.countable_of_inj_on {s : set α} {t : set β} {f : α → β}
+  (hf : maps_to f s t) (hf' : inj_on f s) (ht : countable t) :
+  countable s :=
+have injective (hf.restrict f s t), from (inj_on_iff_injective.1 hf').cod_restrict _,
+⟨@encodable.of_inj _ _ ht.to_encodable _ this⟩
+
+lemma countable.preimage_of_inj_on {s : set β} (hs : countable s) {f : α → β}
+  (hf : inj_on f (f ⁻¹' s)) : countable (f ⁻¹' s) :=
+(maps_to_preimage f s).countable_of_inj_on hf hs
+
+protected lemma countable.preimage {s : set β} (hs : countable s) {f : α → β} (hf : injective f) :
+  countable (f ⁻¹' s) :=
+hs.preimage_of_inj_on (hf.inj_on _)
+
 lemma exists_seq_supr_eq_top_iff_countable [complete_lattice α] {p : α → Prop} (h : ∃ x, p x) :
   (∃ s : ℕ → α, (∀ n, p (s n)) ∧ (⨆ n, s n) = ⊤) ↔
     ∃ S : set α, countable S ∧ (∀ s ∈ S, p s) ∧ Sup S = ⊤ :=

src/data/set/function.lean

@@ -66,6 +66,12 @@ rfl
 variables {s s₁ s₂ : set α} {t t₁ t₂ : set β} {p : set γ} {f f₁ f₂ f₃ : α → β} {g : β → γ}
   {f' f₁' f₂' : β → α} {g' : γ → β}
 
+@[simp] lemma injective_cod_restrict (h : ∀ x, f x ∈ t) :
+  injective (cod_restrict f t h) ↔ injective f :=
+by simp only [injective, subtype.ext_iff, coe_cod_restrict_apply]
+
+alias injective_cod_restrict ↔ _ function.injective.cod_restrict
+
 /-! ### Equality on a set -/
 
 /-- Two functions `f₁ f₂ : α → β` are equal on `s`