## Stream: Coq users

### Topic: Lax–Milgram theorem

#### Koundinya Vajjha (Jun 23 2020 at 20:35):

Hello. I was going through this paper (https://hal.inria.fr/hal-01391578/file/article.pdf) on the formal proof of the Lax-Milgram theorem, and came across this line on page 3:
"Note that in practice, we rely on a version of this theorem on `CompleteNormedModule`, where `is_eq` can be replaced by the native equality and the `phi_distanceable` hypothesis can be removed."

Could someone please explain on why this is true?

#### Koundinya Vajjha (Jun 23 2020 at 20:37):

Relevant definitions are:

``````Require Import Reals Coquelicot.Coquelicot.

Context {V : CompleteSpace}.
Variable f: V -> V.
Variable phi: V -> Prop.

Hypothesis phi_distanceable:
forall (x y:V), phi x -> phi y-> exists M, 0 <= M /\ ball x M y.

Definition is_eq:V→V→Prop := fun a b⇒forall eps:posreal,ball a eps b
``````

#### Koundinya Vajjha (Jun 23 2020 at 20:43):

I'm guessing this has something to do with classical reasoning. In a `CompleteNormedModule`, one can replace `phi_distanceable` by exhibiting an explicit `M = dist x y` where `dist` is the metric induced by the norm. Have I understood this correctly?

#### Cyril Cohen (Jun 23 2020 at 21:19):

@Koundinya Vajjha in the paper you are reading,

• `is_eq` can be read as "arbitrarily closed", which under any separation assumption (from T0) implies equality, in particular normed modules are T2 hence T0 hence `is_eq` impllies equality...
• indeed `phi_distanceable` can be removed in normed modules, because the norm being finite implies any two point are at finite distance from each other.

#### Koundinya Vajjha (Jun 23 2020 at 22:04):

Thank you @Cyril Cohen !

Last updated: Jan 29 2023 at 01:02 UTC