Stream: math-comp analysis

Topic: classical_sets

view this post on Zulip Pierre-Yves Strub (Dec 11 2020 at 10:25):

How can I reduce [set x | P x] = [set x | Q x] to forall x, P <-> Q ?

view this post on Zulip Pierre-Yves Strub (Dec 11 2020 at 10:27):

I answer to myself: predeqE. I think that a predeqP is missing (as well as a in_setP)

view this post on Zulip Cyril Cohen (Dec 11 2020 at 13:45):

Pierre-Yves Strub said:

I answer to myself: predeqE. I think that a predeqP is missing (as well as a in_setP)

I thought I added it....

view this post on Zulip Reynald Affeldt (Dec 17 2020 at 04:22):

maybe use eqEsubset ? (it should be close enough)

Last updated: Oct 13 2024 at 01:02 UTC