mem_closure_iff_clusterPt — Mathlib

English

x is in the closure of s iff x is a cluster point of s with respect to the principal filter.

Русский

Точка x принадлежит замыканию s тогда и только тогда, когда x является кластерной точкой множества s по отношению к ортогональному фильтру.

LaTeX

$$$x \in \overline{s} \iff ClusterPt\ x\ (\mathcal{P} s)$$$

Lean4

theorem mem_closure_iff_clusterPt : x ∈ closure s ↔ ClusterPt x (𝓟 s) :=
  mem_closure_iff_frequently.trans clusterPt_principal_iff_frequently.symm

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