package rocq-num-analysis-lax-milgram
Lax-Milgram theorem
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-num-analysis-2.2.0.tar.gz
sha512=d1996546d967000045e3c58484d6bda8bf4e153f62d6ee42789090c772f0fede197a41b22cfd8253c2729cec515d0bb834d52904d9a38e656858ee7778aac779
Description
This library provides support for the proof of the Lax-Milgram theorem. It is based on classical logic.
Tags
category:Mathematics/Real Calculus and Topology date:2026-03 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: 13 Mar 2026
Dependencies (5)
-
rocq-num-analysis-algebra
= version - rocq-stdlib
-
rocq-core
>= "9.0" & < "9.2~" - coq-stdlib
-
coq-core
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (1)
-
rocq-num-analysis
>= "2.2.0"
Conflicts
None
On This Page