exists_closedBall_inter_eq_singleton_of_discrete

English

In a discrete topological space, around any x ∈ s there exists an open ball that meets s only in {x}.

Русский

В дискретном топологическом пространстве вокруг любого x в s существует открытый шар, пересекающий s только в {x}.

LaTeX

$$$[\\text{DiscreteTopology}(s)] \\Rightarrow \\exists \\varepsilon>0, \\; \\text{Ball}(x,\\varepsilon) \\cap s = \\{x\\}$$$

Lean4

/-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is a closed ball
of positive radius centered at `x` and intersecting `s` only at `x`. -/
theorem exists_closedBall_inter_eq_singleton_of_discrete [DiscreteTopology s] {x : α} (hx : x ∈ s) :
    ∃ ε > 0, Metric.closedBall x ε ∩ s = { x } :=
  nhds_basis_closedBall.exists_inter_eq_singleton_of_mem_discrete hx

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