I have a goal of the

```
H : y < b
=======
\near y, y < b
```

How do I get rid of the `\near`

encapsulation?

`apply: nearW`

?

ah no ok sorry

I don't think it is provable :thinking:

I just tried. but it exhibits a difference between \near y and \near (nbhs y)

It's not because some property is true at `y`

that it is true in a neighboordhood of `y`

(well unless your topology is discrete)

Well, I reduced badly then, but I do have `y \in `]a, b[ `

and I wish to have that `(\forall x \near nbhs y, x < b`

I recommend you do something like

```
near=> x; have : x < y + (b - y)/2%:R.
```

and conclude by transitivity

conclude by transitivity?

The first subgoal uses the proximity of `y`

to `x`

(you can reduce the problem to ` `|x - y| < k`

use `near: x`

and solve it. And the second subgoal is a simple transitivity of `<`

: `x < y + (b - y)/2%:R < b`

(maybe you should use a `suff`

rather than `have`

then :) )

BTW these are questions about mathcomp-analysis, I am moving the discussions there

This topic was moved here from #math-comp users > \near x, something true by Cyril Cohen

This topic was moved by Cyril Cohen to #math-comp analysis > \near x, something true

I still don't understand the justification given by Cyril "this is probably not true". Because in the formula `\near y, ...`

`y`

is not a binder, is it?

This topic was moved here from #math-comp users > \near x, something true by Cyril Cohen

Yves Bertot said:

I still don't understand the justification given by Cyril "this is probably not true". Because in the formula

`\near y, ...`

`y`

is not a binder, is it?

It's free on the left and bound on the right, it's a tricky one...

Maybe we should remove it...

`\near y, P y`

is equilvalent to `\forall x \near y, P x`

Last updated: Aug 19 2022 at 20:03 UTC