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: Jun 22 2024 at 16:02 UTC