Stream: math-comp analysis

Topic: question about using cancel in a \near context


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

view this post on Zulip Laurent Théry (Jun 04 2021 at 08:37):

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

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

view this post on Zulip Yves Bertot (Jun 04 2021 at 08:54):

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

view this post on Zulip Yves Bertot (Jun 04 2021 at 08:55):

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

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

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

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

Yes.

view this post on Zulip Yves Bertot (Jun 04 2021 at 09:02):

thanks

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

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

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

view this post on Zulip Laurent Théry (Jun 04 2021 at 09:20):

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

view this post on Zulip Cyril Cohen (Jun 04 2021 at 09:21):

Maybe we should indeed

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

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

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

view this post on Zulip Yves Bertot (Jun 04 2021 at 09:29):

Agreed.

view this post on Zulip 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: Aug 11 2022 at 03:02 UTC