Commit 2020-09-26 10:16 b8b6f5dd
View on Github →chore(order/filter/archimedean): move&generalize a few lemmas (#4275)
tendsto_coe_nat_real_at_top_iff:tendsto_coe_nat_at_top_iff, generalize to a linear ordered archimedean semiring;tendsto_coe_nat_real_at_top_at_top:tendsto_coe_nat_at_top_at_top, generalize to a linear ordered archimedean semiring;tendsto_coe_int_real_at_top_iff:tendsto_coe_int_at_top_iff, generalize to a linear ordered archimedean ring;tendsto_coe_int_real_at_top_at_top:tendsto_coe_int_at_top_at_top, generalize to a linear ordered archimedean ring;- add versions for
ℚ; - golf the proof of
tendsto_at_top_embedding.