English
Alexandrov-discreteness of α is equivalent to nhds of every point being the principal nhdsKer singleton.
Русский
Александрово-дискретность пространства α эквивалентна тому, что для каждого a выполнено nhds a = nhds Ker {a}.
LaTeX
$$AlexandrovDiscrete α ↔ (∀ a, 𝓝 a = 𝓟 (nhdsKer { a }))$$
Lean4
theorem alexandrovDiscrete_iff_nhds : AlexandrovDiscrete α ↔ (∀ a : α, 𝓝 a = 𝓟 (nhdsKer { a }))
where
mp _ a := principal_nhdsKer_singleton a |>.symm
mpr
hα :=
by
simp only [alexandrovDiscrete_iff_isClosed, isClosed_iff_clusterPt, ClusterPt, funext hα, inf_principal,
principal_neBot_iff]
intro S hS a ha
rw [sUnion_eq_biUnion, inter_iUnion₂, nonempty_biUnion] at ha
obtain ⟨s, hs, has⟩ := ha
specialize hS s hs a has
exact mem_sUnion_of_mem hS hs
