Stream: math-comp analysis

Topic: question about using cancel in a \near context

Yves Bertot (Jun 04 2021 at 08:30):

I understand {in ]a, b[, cancel f g} means forall x, x \in ]a, b[ -> g (f x) = x}. But if I write something like
\forall y \near x, cancel f g, I don't get the intended meaning, and I am puzzled on how to express that I want injectivity to be asserted only in a neighborhood of x.

Laurent Théry (Jun 04 2021 at 08:37):

forall y \near x, g (f y) = y?

Yves Bertot (Jun 04 2021 at 08:39):

Yes, I will have to do that, thanks. I wanted to use the cancel notion, but it does not fit, and prop_in1 (the function behind {in _, _} notation manages the trick thanks to phantom technology that I don't grasp.

Yves Bertot (Jun 04 2021 at 08:54):

Okay, I found a solution:
\forall y \near x, {for y, cancel f g}

Yves Bertot (Jun 04 2021 at 08:55):

I think I start to understand a few things about phantoms.

Yves Bertot (Jun 04 2021 at 08:57):

Then, during the proof the {for _, _} can be gotten rid of using rewrite forE. These are defined in coq.ssr.ssrbool.v

Cyril Cohen (Jun 04 2021 at 08:59):

Yves Bertot said:

Okay, I found a solution:
\forall y \near x, {for y, cancel f g}

Can you use {near x, cancel f g} ?

Yes.

thanks

Yves Bertot (Jun 04 2021 at 09:06):

So writing that an injective function is monotone would be written this way:

Lemma near_injective_monotone (f g : R -> R) (x : R) :
{near x, cancel f g} ->
{near x & x, forall y z, y < z -> f y < f z} \/
{near x & x, forall z y, z < y -> f z < f y}.


Yves Bertot (Jun 04 2021 at 09:08):

Sorry, I included too many permutations of y and z. The right statement should be:

Lemma near_injective_monotone (f g : R -> R) (x : R) :
{near x, cancel f g} ->
{near x & x, forall y z, y < z -> f y < f z} \/
{near x & x, forall y z, y < z -> f z < f y}.


Cyril Cohen (Jun 04 2021 at 09:19):

Lemma near_injective_monotone (f : R -> R) (x : R) : {near x, injective f} ->
{near x &, {mono f : y z / y <= z}} \/ {near x &, {mono f : y z /~ y <= z}}


Laurent Théry (Jun 04 2021 at 09:20):

Should we not introduce a notion of monotonous function rather than having these horrible \/?

Cyril Cohen (Jun 04 2021 at 09:21):

Maybe we should indeed

Cyril Cohen (Jun 04 2021 at 09:23):

Cyril Cohen said:

Lemma near_injective_monotone (f : R -> R) (x : R) : {near x, injective f} ->
{near x &, {mono f : y z / y <= z}} \/ {near x &, {mono f : y z /~ y <= z}}


Also aren't you missing a continuity hypothesis? and why is it near rather than in some interval?

Yves Bertot (Jun 04 2021 at 09:24):

I would be more comfortable with within some interval, I was wondering whether using near would be more idiomatic.

Cyril Cohen (Jun 04 2021 at 09:27):

Yves Bertot said:

I would be more comfortable with within some interval, I was wondering whether using near would be more idiomatic.

It would be less general, the theorem is global (on some interval) not local. (i.e. the neighborhood you consider in the conclusion can be the same as the one from the hypotheses)

Agreed.

Yves Bertot (Jun 04 2021 at 09:35):

Still, I don't see how to use a monotone definition and make it work with the prop_in2 function, because the sense of monotony has to be fixed once and for all.

Last updated: Jun 22 2024 at 16:02 UTC