English
CodiscreteWithin respects image under analytic maps: the push-forward is codiscreteWithin.
Русский
Кодискретность сохраняется под аналитическими отображениями: образ в кодискретном виде сохраняет кодискретность.
LaTeX
$$$$map\\_codiscreteWithin(f) (U) \\le codiscreteWithin(f''U).$$$$
Lean4
/-- Preimages of codiscrete sets, filter version: if `f` is analytic on a neighbourhood of `U` and
not locally constant, then the push-forward of the filter of sets codiscrete within `U` is less
than or equal to the filter of sets codiscrete within `f '' U`.
Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
-/
theorem map_codiscreteWithin {U : Set 𝕜} {f : 𝕜 → E} (hfU : AnalyticOnNhd 𝕜 f U)
(h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)) : map f (codiscreteWithin U) ≤ (codiscreteWithin (f '' U)) := fun _ hs ↦
mem_map.1 (preimage_mem_codiscreteWithin hfU h₂f hs)
