Just to notify that @Théo Vignon has recently formalized Banach-Steinhaus theorem and Baire's theorem based on the recent release of math-comp Analysis : https://github.com/tvignon/StageL3

Last updated: Jun 22 2024 at 16:02 UTC