Is Lax-Milgram true without the separability assumption?

Question

I read the Lax-Milgram Theorem in the Navier-Stokes Equations by Temam:

Let $X$ be a separable Hilbert space (norm $\|\cdot\|_X$) and let $$ a:X\times X\to\Bbb{R} $$ be a bilinear continuous coercive form; that is, there exist $c,C>0$, such that for all $u,v\in X$, we have \begin{align} |a(u,v)|&\leq C\|u\|_X\|v\|_X&\text{(continuous)}\\ a(u,u)&\geq c\|u\|_X^2 &\text{(coersive)} \end{align} Then, for each continuous functional $\lambda$ on $X$, there exists a unique element $u\in X$ such that $$ a(u,v)=\langle \lambda,v\rangle\quad\text{for all }v\in X. $$

The proof of existence in his book explicitly exploits the separability of the space. Some people define Hilbert spaces with the separability assumption. Is this theorem true without the separability assumption? (If yes, would you come up with some cited references?)

Answer 1

A reference without the separability requirement: Elements of Nonlinear Analysis, by Michel Chipot, namely Theorem 3.2 in page 41.

Actually, you may have a look at Temam's book "Infinite-Dimensional Dynamical Systems in Mechanics and Physics", more precisely at Theorem II.2.1 in page 54. It also doesn't use separability, and curiously the proof goes by showing that a certain map is a contraction.