search

ImperialCollegeLondon / real-number-game

A gamification of the theorems in MATH40002 Analysis 1
Apache License 2.0
79 stars 8 forks source link

Solution to const multiplication of lim. #1

Closed thyrgle closed 4 years ago

thyrgle commented 4 years ago

Hello,

I am fairly new to Lean but I decided to try implementing the theorem limit.const_mult:

Given a sequence (a_n) with limit L, the sequence defined by (c*a_n) should have the limit c*L.

This seemed like a nice next step from showing that a limit is unique. The theorem compiles, but I am not sure if you find it too verbose or just not quality enough. Feel to close or make changes to this pull request if you feel it is not of high enough quality.

Thank you.

stanescuUW commented 4 years ago

@thyrgle Thank you for your PR contribution to the real number game and sorry for the long delay. We couldn't merge your file any more because of the changes in mathlib. We did use your idea however and will acknowledge it to our best.