In a context where `I`

is an interval on `R`

a realType, I would like to talk about the interior of the image of this interval by a function. I have no better solution than :

```
interior [set f x | x in [set x | x \in I]]%classic
```

or

```
interior f @` [set x | x \in I]]%classic
```

And I still do not manage to combine this with the {in _, _} notation, because prop_in expects a boolean predicate. Do you have any suggestions?

Eventually, I get to the following situation when combining with `prop_in1`

```
{in ([set y | y in (interior [set f x | x in [set x | x \in I]])])%classic,
continuous g}
```

ok, PR 371 has a full section to define the concept `set_of_itv`

, together with rewriting rules.

note that this in a part of the file that has not yet been the object of much scrutiny but it should be soon now that the top of the file is being PRed

we couldn’t find easily a more transparent way to accommodate the switch interval<->set, but set_of_itv and its instrumentation did support more lemmas so at least it should provide a testbed for experimenting other solutions

Last updated: Jun 25 2024 at 19:01 UTC