Yves Bertot (Jul 23 2021 at 13:07): Yves Bertot (Jul 23 2021 at 13:07):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?
Yves Bertot (Jul 23 2021 at 13:38):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.
Reynald Affeldt (Jul 23 2021 at 14:36):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
Reynald Affeldt (Jul 23 2021 at 14:40):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: Apr 19 2024 at 00:02 UTC