I can write
Variable R : realType.
Lemma near_in_interval (a b : R) :
{in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
but in the same context, I can't write
Lemma near_0_in_interval (a b : R) :
{in `]a, b[, forall y, \forall z \near 0, (z + y : R) \in `]a, b[}.
Is there a simple type annotation to add so that it works?
I guess it does not know the type of 0
Did you open ring_scope
?
or try (0 : R)
Thanks Laurent, your hint does the trick.
And thanks Kazuhiko, but ring_scope was already open.
Last updated: Mar 29 2024 at 11:01 UTC