ThmDex – An index of mathematical definitions, results, and conjectures.
Result R458 on D97: Open set
Open set iff contains an open neighbourhood at every point