mem_interior_iff_not_clusterPt_compl

English

x ∈ interior s iff x is not a cluster point of sᶜ.

Русский

Точка x принадлежит interior s тогда и только тогда, когда x не является кластерной точкой комплемента sᶜ.

LaTeX

$$$x \in \operatorname{Int}(s) \iff \neg ClusterPt\ x\ (\mathcal{P} s^{\complement})$$$

Lean4

theorem mem_interior_iff_not_clusterPt_compl : x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ) := by
  rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]

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