Stream: math-comp analysis

Topic: \near x, something true


view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Jun 01 2021 at 09:52):

apply: nearW ?

view this post on Zulip Cyril Cohen (Jun 01 2021 at 09:52):

ah no ok sorry

view this post on Zulip Cyril Cohen (Jun 01 2021 at 09:54):

I don't think it is provable :thinking:

view this post on Zulip Yves Bertot (Jun 01 2021 at 09:54):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yves Bertot (Jun 01 2021 at 10:01):

conclude by transitivity?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Jun 01 2021 at 10:04):

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

view this post on Zulip Cyril Cohen (Jun 01 2021 at 10:07):

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

view this post on Zulip Notification Bot (Jun 01 2021 at 10:08):

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

view this post on Zulip Notification Bot (Jun 01 2021 at 10:08):

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

view this post on Zulip 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?

view this post on Zulip Notification Bot (Jun 01 2021 at 14:17):

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

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (Jun 01 2021 at 14:18):

Maybe we should remove it...

view this post on Zulip 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