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: Mar 28 2024 at 15:01 UTC