inseparable_iff_clusterPt_uniformity

English

Two points x and y in α are inseparable if and only if the pair (x, y) is a cluster point for the uniformity 𝓤α on α × α.

Русский

Две точки x и y в α неразделимы тогда и только тогда, когда пара (x, y) является кластерной точкой для равномерности 𝓤α на α × α.

LaTeX

$$$\text{Inseparable}(x,y) \iff \text{ClusterPt}( (x,y) , 𝓤α )$$$

Lean4

theorem inseparable_iff_clusterPt_uniformity {x y : α} : Inseparable x y ↔ ClusterPt (x, y) (𝓤 α) :=
  by
  refine ⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩
  simp_rw [uniformity_hasBasis_closed.inseparable_iff_uniformity, isClosed_iff_clusterPt]
  exact fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU

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