English
If f is a closed map and a property p holds eventually near every x in the fiber over y0, then for y near y0, p holds on the fiber over y.
Русский
Если f - замкнутое отображение и свойство p выполняется близко к каждому x в волокне над y0, то приближаясь к y0, свойство p выполняется на волокне над y.
LaTeX
$$$IsClosedMap f \\to \\forall {p:X\\to Prop} (y_0:Y), (\\forall x_0 \\in f^{-1}\\{y_0\},\\ ∀ᶠ x in 𝓝 x_0, p x) \\to \\\\ ∀ᶠ y in 𝓝 y_0, \\forall x \\in f^{-1}\\{y}, p x$$$
Lean4
/-- Assume `f` is a closed map. If some property `p` holds around every point in the fiber of `f`
at `y₀`, then for any `y` close enough to `y₀` we have that `p` holds on the fiber at `y`. -/
theorem eventually_nhds_fiber (hf : IsClosedMap f) {p : X → Prop} (y₀ : Y)
(H : ∀ x₀ ∈ f ⁻¹' { y₀ }, ∀ᶠ x in 𝓝 x₀, p x) : ∀ᶠ y in 𝓝 y₀, ∀ x ∈ f ⁻¹' { y }, p x :=
by
rw [← eventually_nhdsSet_iff_forall] at H
replace H := H.filter_mono hf.comap_nhds_le
rwa [eventually_comap] at H
