Commit 2020-12-18 12:03 74b58397

chore(topology/algebra/ordered): generalize tendsto_at_top_add_left etc (#5398)

• generalize some lemmas from linear_ordered_ring to linear_ordered_add_comm_group;
• rename them to allow dot notation; the new names are filter.tendsto.add_at_* and filter.tendsto.at_*_add, where * is top or bot;
• generalize infi_unit and supr_unit to conditionally_complete_lattice, add [unique α] versions;
• in a subsingleton, both at_top and at_bot are equal to ⊤; these lemmas are useful for the nontriviality tactic.