English
Let X be a topological space and F a filter on X. The cluster-point property of a point x with respect to the lifted-closure of F is equivalent to the cluster-point property with respect to F itself; that is, x is a cluster point of F lifted by closure if and only if x is a cluster point of F.
Русский
Пусть X – топологическое пространство, F – фильтр на X. Точка x является кластерной точкой фильтра F после подъема через замыкание, эквивалентно тому, что x является кластерной точкой самого фильтра F; то есть x является кластерной точкой F ⇔ x является кластерной точкой F, разукомпозированного через замыкание.
LaTeX
$$$ \\mathrm{ClusterPt}\\bigl(x, F^{\\mathrm{lift'}\\,\\mathrm{closure}}\\bigr) \\iff \\mathrm{ClusterPt}(x, F) $$$
Lean4
@[simp]
theorem clusterPt_lift'_closure_iff {F : Filter X} : ClusterPt x (F.lift' closure) ↔ ClusterPt x F := by
simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]
