English
If f is analytic on a nhd of U and is never locally constant, then the push-forward of codiscreteWithin U under f is contained in codiscreteWithin (f''U).
Русский
Если f аналитична на окрестности U и никогда не является локально константной, то образ codiscreteWithin(U) под f содержится в codiscreteWithin (f''U).
LaTeX
$$$$\\operatorname{map} f (\\operatorname{codiscreteWithin} U) \\le (\\operatorname{codiscreteWithin} (f''U)).$$$$
Lean4
/-- Preimages of codiscrete sets, local filter version: if `f` is analytic at `x` and not locally
constant, then the push-forward of the punctured neighbourhood filter `𝓝[≠] x` is less than or
equal to the punctured neighbourhood filter `𝓝[≠] f x`. -/
theorem map_nhdsNE {x : 𝕜} {f : 𝕜 → E} (hfx : AnalyticAt 𝕜 f x) (h₂f : ¬EventuallyConst f (𝓝 x)) :
(𝓝[≠] x).map f ≤ (𝓝[≠] f x) := fun _ hs ↦ mem_map.1 (preimage_of_nhdsNE hfx h₂f hs)
