package rocq-num-analysis-lax-milgram
Lax-Milgram theorem
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-num-analysis-2.1.0.tar.gz
sha512=515ad6799b3e8916beaca37c65a9d25e3f0e1b09d38c44afa8809f41ffcc9e39c92f241afff171d08e0c31bd71724bb3f21f4f4ae3294ffa44828203a468cca8
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-12 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: 27 Nov 2025
Dependencies (4)
-
rocq-num-analysis-algebra
= version - rocq-stdlib
-
rocq-core
>= "9.0" & < "9.2~" -
coq
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (1)
-
rocq-num-analysis
>= "2.1.0"
Conflicts
None
On This Page