Zulip Chat Archive

Stream: new members

Topic: real analysis


Pedro Castilho (Nov 09 2020 at 21:35):

Does anyone know some good material for real analysis with exercises and solutions in lean

Alex J. Best (Nov 09 2020 at 22:12):

The #tutorials project has a bit of sequences, limits etc.

Kevin Buzzard (Nov 09 2020 at 22:13):

I'm giving a talk on the Xena project discord about doing analysis in Lean on Thursday evening UK. There is the tutorial project. I should write the real number game at some point :-/ We have a lot of material now

Pedro Castilho (Nov 09 2020 at 22:14):

@Alex J. Best I saw a bit of that in the tutorial, i wanted to se more

Pedro Castilho (Nov 09 2020 at 22:15):

@Kevin Buzzard can I came to the talk? is there a link I can use?

Kevin Buzzard (Nov 10 2020 at 16:41):

(replied via DM)


Last updated: Dec 20 2023 at 11:08 UTC