mathlib

0980bacb - chore(topological_space/sober): use `namespace` and `variables`, golf (#15042)

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.