Commit 2020-08-21 20:49 4c04f0bb
View on Github →feat(topology/algebra/ordered): sum of functions with limits at_top and cst (#3833)
Two functions which tend to at_top have sum tending to at_top. Likewise if one tends to at_top and one tends to a constant.
Also made a couple of edits relating to this conversation about no_top for algebraic structures: