Commit 2022-07-11 14:26 0980bacb

chore(topological_space/sober): use namespace and variables, golf (#15042)

API

• Add is_generic_point_iff_specializes, is_generic_point.specializes_iff_mem.
• Make is_generic_point.is_closed etc protected.

Style

• Use namespace is_generic_point.
• Move implicit arguments to variables.
• Move explicit (h : is_generic_point x S) from variables to each lemma.
• Golf some proofs.