[zozbot234]

I don't quite get how it's supposed to introduce calculus/analysis - the introductory chapters just start talking about metric spaces without even bothering to properly introduce the real numbers or their peoperties. I don't think that's quite sensible. For comparison, mathlib4 of course does it right by starting from topological spaces - and it manages to nicely simplify things throughout, by defining a basic "tends to" notion using set-theoretic filters.