English
For a filter F on X and a point y ∈ Y, y is a cluster point of f with respect to F if and only if the infimum of F lifted with closure and the principal filter at f⁻¹({y}) is nonempty: MapClusterPt y F f ⇔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' { y })).NeBot.
Русский
Для фильтра F на X и точки y ∈ Y точка y является кластерной точкой относительно f∘F тогда и только тогда, когда пересечение возведённого замыкания F и главного фильтра в области определения f⁻¹({y}) непусто: MapClusterPt y F f ⇔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' { y })).NeBot.
LaTeX
$$$ MapClusterPt\, y\, F\, f \iff \big( (F.lift'\;closure) \;\sqcap\; 𝓟\,(f^{-1}\{y\}) \big).\mathrm{NeBot} $$$
Lean4
theorem mapClusterPt_iff_lift'_closure {F : Filter X} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : Y} :
MapClusterPt y F f ↔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' { y })).NeBot := by
rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont, ← comap_principal, ←
map_neBot_iff f, Filter.push_pull, principal_singleton]
