Commit 2021-03-09 08:12 6dec23b2

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