Proof of the Lax-Milgram Theorem

This page is dedicated to the formal proof in Coq of the Lax-Milgram Theorem.

The full code is downloadable here.

You may also want to browse the library by the index or by clicking the dependence graph: