mathlib3

237b1ea5 - feat(analysis/specific_limits): proof of harmonic series diverging and preliminaries (#3233)

feat(analysis/specific_limits): proof of harmonic series diverging and preliminaries (#3233) This PR is made of two parts : - A few new generic lemmas, mostly by @PatrickMassot , in `order/filter/at_top_bot.lean` and `topology/algebra/ordered.lean` - Definition of the harmonic series, basic lemmas about it, and proof of its divergence, in `analysis/specific_limits.lean` Zulip : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Harmonic.20Series.20Divergence/near/201651652 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>