package rocq-num-analysis-lax-milgram
Lax-Milgram theorem
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-num-analysis-2.0.0.tar.gz
sha512=b2453dc67f2b716ea0a473ca9942eacd3e1eed29493395e35eac5b997e840ec95ed4b028a416b1e92c9a88403cf01812f7744fbc1f0dc8fa8596a2d5c4b8b9b1
Description
This library provides support for the proof of the Lax-Milgram theorem. It is based on classical logic.
Tags
category:Math/Real Calculus and Topology date:2025-06 logpath:NumAnalysis.LM keyword:fixed point theorem (in a Banach space) keyword:orthogonal projection keyword:orthogonal complement keyword:Riesz-Fréchet representation theorem keyword:Lax-Milgram theorem keyword:Céa's lemmaPublished: 23 Jun 2025
Dependencies (3)
-
rocq-num-analysis-algebra
= version -
rocq-prover
>= "9.0" & < "9.1~" -
coq
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (1)
Conflicts
None
On This Page