A project to formalize the theory of o-minimal structures in Lean.
-
Semilinear sets form an o-minimal structure.
-
Lemma 1 of the monotonicity theorem.
-
Definable choice (
sorry-free draft version).
-
ominis a playground for new ideas, and may contain unfinished proofs or even definitions, temporary names, and so on. -
src/o_minimalis the "official" formalization and is supposed to avoidsorry, although it is still at a highly experimental phase. -
src/for_mathlibcontains supporting developments.
- [vdD] Lou van den Dries, Tame topology and o-minimal structures. https://doi.org/10.1017/CBO9780511525919