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?

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
```

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?

@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.

Thank you @Cyril Cohen !

Last updated: Jan 29 2023 at 01:02 UTC