English
Let s be a discrete subset and x ∈ s. There exists an open set U with IsOpen U and U ∩ s = {x}.
Русский
Пусть s — дискретное подмножество и x ∈ s. Тогда существует открытое множество U такое, что IsOpen(U) и U ∩ s = {x}.
LaTeX
$$$ \\forall X [TopologicalSpace X] {s} [DiscreteTopology s] {x} (hx : x ∈ s), \\exists U, IsOpen U \\wedge (U \\cap s) = {x}. $$$
Lean4
/-- Let `x` be a point in a discrete subset `s` of a topological space, then there exists an open
set that only meets `s` at `x`. -/
theorem isOpen_inter_eq_singleton_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
∃ U : Set X, IsOpen U ∧ U ∩ s = { x } :=
by
obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hx
obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds
refine ⟨t, ht_open, Set.Subset.antisymm ?_ ?_⟩
· exact hU_inter ▸ Set.inter_subset_inter_left s ht_sub
· rw [Set.subset_inter_iff, Set.singleton_subset_iff, Set.singleton_subset_iff]
exact ⟨ht_x, hx⟩
