Stream: math-comp analysis

Topic: Combining prop_in1 and interior


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

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

view this post on Zulip Yves Bertot (Jul 23 2021 at 14:08):

ok, PR 371 has a full section to define the concept set_of_itv, together with rewriting rules.

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

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