frequently — Mathlib

English

If hx is a cluster point and hp holds eventually near x, then there are frequently points in F satisfying p.

Русский

Если x — кластерная точка и hp выполняется часто вблизи x, тогда в F часто встречаются точки с свойством p.

LaTeX

$$$\operatorname{ClusterPt} x F \\Rightarrow \\operatorname{Frequently}(\\lambda y, p(y)) F$$

Lean4

theorem frequently {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ y in 𝓝 x, p y) : ∃ᶠ y in F, p y :=
  clusterPt_iff_frequently.mp hx {y | p y} hp

Похожие утверждения