## Stream: math-comp analysis

### Topic: \near x, something true

#### Yves Bertot (Jun 01 2021 at 09:49):

I have a goal of the

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


How do I get rid of the \near encapsulation?

#### Cyril Cohen (Jun 01 2021 at 09:52):

apply: nearW ?

ah no ok sorry

#### Cyril Cohen (Jun 01 2021 at 09:54):

I don't think it is provable :thinking:

#### Yves Bertot (Jun 01 2021 at 09:54):

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

#### Cyril Cohen (Jun 01 2021 at 09:54):

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)

#### Yves Bertot (Jun 01 2021 at 09:56):

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

#### Cyril Cohen (Jun 01 2021 at 09:58):

I recommend you do something like

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


and conclude by transitivity

#### Yves Bertot (Jun 01 2021 at 10:01):

conclude by transitivity?

#### Cyril Cohen (Jun 01 2021 at 10:03):

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

#### Cyril Cohen (Jun 01 2021 at 10:04):

(maybe you should use a suff rather than have then :) )

#### Cyril Cohen (Jun 01 2021 at 10:07):

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

#### Notification Bot (Jun 01 2021 at 10:08):

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

#### Notification Bot (Jun 01 2021 at 10:08):

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

#### Yves Bertot (Jun 01 2021 at 12:40):

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?

#### Notification Bot (Jun 01 2021 at 14:17):

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

#### Cyril Cohen (Jun 01 2021 at 14:18):

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

#### Cyril Cohen (Jun 01 2021 at 14:18):

Maybe we should remove it...

#### Cyril Cohen (Jun 01 2021 at 14:18):

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

Last updated: Aug 19 2022 at 20:03 UTC