English
If a point x has a finite neighborhood, then {x} is open.
Русский
Если точка x имеет конечное соседство, то множество {x} открыто.
LaTeX
$$$\text{IsOpen}({x}) \,\text{в случае} \, s \in \mathcal{N}(x) \text{ и } s\text{ finite}$$$
Lean4
/-- A point with a finite neighborhood has to be isolated. -/
theorem isOpen_singleton_of_finite_mem_nhds [T1Space X] (x : X) {s : Set X} (hs : s ∈ 𝓝 x) (hsf : s.Finite) :
IsOpen ({ x } : Set X) :=
by
have A : { x } ⊆ s := by simp only [singleton_subset_iff, mem_of_mem_nhds hs]
have B : IsClosed (s \ { x }) := (hsf.subset diff_subset).isClosed
have C : (s \ { x })ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl
have D : { x } ∈ 𝓝 x := by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C
rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D
