Formalization of Michael Selection Theorem

Stream: general

[Riccardo Formenti]

I recently completed a formalization of Michael Selection Theorem, a result in the theory of set-valued functions (also known as correspondences) which is relevant to functional analysis, dynamical systems theory, fixed point theory, game theory. In doing so, I had to formalize basic topological definitions on the continuity of set-valued maps and a number of small lemmas.

I'm new to the community and would very much appreciate some guidance on how to contribute my results to Mathlib.

[Kim Morrison]

As many PRs as it takes, ideally ~100 lines of new material in each PR, make sure that it passes CI and appears on the #queue, and if you're sad something it not getting attention create a thread at #PR reviews explaining the context and what is coming next!

The review process can be time consuming, and sometimes painful, but you will learn a lot and the material will be improved by going through it!

[Johan Commelin]

@Riccardo Formenti Welcome! The bottom-most part of the side menu on the community site contains some docs that I hope are useful. See https://leanprover-community.github.io/

image.png