English
For any set s, the preimage exp^{-1}(s) is countable if and only if s is countable.
Русский
Для любого множества s обратное изображение exp^{-1}(s) конечно счётно тогда и только тогда, когда само множество s счётно.
LaTeX
$$$(\exp^{-1} s).\operatorname{Countable} \iff s.\operatorname{Countable}$$$
Lean4
@[simp]
theorem countable_preimage_exp {s : Set ℂ} : (exp ⁻¹' s).Countable ↔ s.Countable :=
by
refine ⟨fun hs => ?_, fun hs => ?_⟩
· refine ((hs.image exp).insert 0).mono ?_
rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.diff_eq, ← Set.union_singleton, Set.diff_union_self]
exact Set.subset_union_left
· rw [← Set.biUnion_preimage_singleton]
refine hs.biUnion fun z hz => ?_
rcases em (∃ w, exp w = z) with (⟨w, rfl⟩ | hne)
· simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]
exact Set.countable_iUnion fun m => Set.countable_singleton _
· push_neg at hne
simp [Set.preimage, hne]
