English
A dual result to eventually_nhds_fiber: from frequent occurrence around y0, deduce a fiber property at some y0.
Русский
Другая версия frequently_nhds_fiber: из частого появления около y0 выводится свойство в волокне над y0.
LaTeX
$$$IsClosedMap f \\to ∀ {p:X→Prop} (y_0:Y),\\ \\text{Frequent}(y)\\to ∃ x_0 ∈ f^{-1}\\{y_0\\},\\?^p x$$$
Lean4
/-- Assume `f` is a closed map. If there are points `y` arbitrarily close to `y₀` such that `p`
holds for at least some `x ∈ f ⁻¹' {y}`, then one can find `x₀ ∈ f ⁻¹' {y₀}` such that there
are points `x` arbitrarily close to `x₀` which satisfy `p`. -/
theorem frequently_nhds_fiber (hf : IsClosedMap f) {p : X → Prop} (y₀ : Y) (H : ∃ᶠ y in 𝓝 y₀, ∃ x ∈ f ⁻¹' { y }, p x) :
∃ x₀ ∈ f ⁻¹' { y₀ }, ∃ᶠ x in 𝓝 x₀, p x := by
/-
Note: this result could also be seen as a reformulation of `isClosedMap_iff_clusterPt`.
One would then be able to deduce the `eventually` statement,
and then go back to `isClosedMap_iff_comap_nhdsSet_le`.
Ultimately, this makes no difference.
-/
revert H
contrapose
simpa only [not_frequently, not_exists, not_and] using hf.eventually_nhds_fiber y₀
