Stream: math-comp analysis

Topic: A \forall .. \near .. formula that resists acceptation


view this post on Zulip Yves Bertot (Jun 02 2021 at 06:59):

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?

view this post on Zulip Laurent Théry (Jun 02 2021 at 07:05):

I guess it does not know the type of 0

view this post on Zulip Kazuhiko Sakaguchi (Jun 02 2021 at 07:06):

Did you open ring_scope?

view this post on Zulip Laurent Théry (Jun 02 2021 at 07:07):

or try (0 : R)

view this post on Zulip Yves Bertot (Jun 02 2021 at 07:52):

Thanks Laurent, your hint does the trick.

view this post on Zulip Yves Bertot (Jun 02 2021 at 07:53):

And thanks Kazuhiko, but ring_scope was already open.


Last updated: Mar 29 2024 at 11:01 UTC