English
If f is analytic on nhds of U and f is never locally constant on U, then the preimage of a codiscrete subset of f''U is codiscrete within U.
Русский
Если f аналитична на nhds(U) и не локально константна, то предобраз кодискретного подмножества f''U в U кодискретен.
LaTeX
$$$$f^{-1}(s) \\in \\mathrm{codiscreteWithin}(U)\\quad\\text{for } s\\in \\mathrm{codiscreteWithin}(f''U).$$$$
Lean4
/-- Preimages of codiscrete sets: if `f` is analytic on a neighbourhood of `U` and not locally constant,
then the preimage of any subset codiscrete within `f '' U` is codiscrete within `U`.
See `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` for the special case that `s` is the
complement of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
-/
theorem preimage_mem_codiscreteWithin {U : Set 𝕜} {s : Set E} {f : 𝕜 → E} (hfU : AnalyticOnNhd 𝕜 f U)
(h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)) (hs : s ∈ codiscreteWithin (f '' U)) : f ⁻¹' s ∈ codiscreteWithin U :=
by
simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff] at *
intro x hx
apply mem_of_superset ((hfU x hx).preimage_of_nhdsNE (h₂f x hx) (hs (f x) (by tauto)))
rw [preimage_union, preimage_compl]
apply union_subset_union_right (f ⁻¹' s)
intro x hx
simp only [mem_compl_iff, mem_preimage, mem_image, not_exists, not_and] at hx ⊢
tauto
