lean-omin

A project to formalize the theory of o-minimal structures in Lean.

Current features

Semilinear sets form an o-minimal structure.
Lemma 1 of the monotonicity theorem.
Definable choice (sorry-free draft version).

Directory layout

omin is a playground for new ideas, and may contain unfinished proofs or even definitions, temporary names, and so on.
src/o_minimal is the "official" formalization and is supposed to avoid sorry, although it is still at a highly experimental phase.
src/for_mathlib contains supporting developments.

References

[vdD] Lou van den Dries, Tame topology and o-minimal structures. https://doi.org/10.1017/CBO9780511525919