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.
forall y \near x, g (f y) = y
?
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.
Okay, I found a solution:
\forall y \near x, {for y, cancel f g}
I think I start to understand a few things about phantoms.
Then, during the proof the {for _, _}
can be gotten rid of using rewrite forE.
These are defined in coq.ssr.ssrbool.v
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
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}.
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}.
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}}
Should we not introduce a notion of monotonous function rather than having these horrible \/?
Maybe we should indeed
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?
I would be more comfortable with within some interval, I was wondering whether using near
would be more idiomatic.
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.
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: Oct 13 2024 at 01:02 UTC