mathlib

6dec23b2 - chore(topology/algebra/ordered): use dot notation, golf some proofs (#6595)

chore(topology/algebra/ordered): use dot notation, golf some proofs (#6595) Use more precise typeclass arguments here and there, golf some proofs, use dot notation. ### Renamed lemmas * `is_lub_of_is_lub_of_tendsto` → `is_lub.is_lub_of_tendsto`; * `is_glb_of_is_glb_of_tendsto` → `is_glb.is_glb_of_tendsto`; * `is_glb_of_is_lub_of_tendsto` → `is_lub.is_glb_of_tendsto`; * `is_lub_of_is_glb_of_tendsto` → `is_glb.is_lub_of_tendsto`; * `mem_closure_of_is_lub` → `is_lub.mem_closure`; * `mem_of_is_lub_of_is_closed` → `is_lub.mem_of_is_closed`, `is_closed.is_lub_mem`; * `mem_closure_of_is_glb` → `is_glb.mem_closure`; * `mem_of_is_glb_of_is_closed` → `is_glb.mem_of_is_closed`, `is_closed.is_glb_mem`; ### New lemmas * `is_lub.inter_Ici_of_mem` * `is_glb.inter_Iic_of_mem` * `frequently.filter_mono` * `is_lub.frequently_mem` * `is_lub.frequently_nhds_mem` * `is_glb.frequently_mem` * `is_glb.frequently_nhds_mem` * `is_lub.mem_upper_bounds_of_tendsto` * `is_glb.mem_lower_bounds_of_tendsto` * `is_lub.mem_lower_bounds_of_tendsto` * `is_glb.mem_upper_bounds_of_tendsto` * `diff_subset_closure_iff`