Hello,
I wrote a note on notions of convergence of sequences of functions in mathematics.
My goal was to see by myself if many definitions were possible.
I did found quite a few definitions at the end.
Maybe the approximate notions of convergence would be more interesting to computer scientists than mathematicians.
I was expecting to write 3 pages or so, and my note is 9 pages long now.
I thought this note would be better completed as a package of definitions and proofs in Rocq or LEAN. And that it could maybe be a good exercise for students to code it in Rocq.
Here are the links if you want to check if it can be interesting.
French version:
English version:
Best regards,
Laurent Lyaudet