On Friday, June 14, 2019 at 3:24:42 PM UTC+2, Thierry Arnoux wrote:
>
> Hi Jon & Benoît,
>
> I've created the deduction version of that theorem
> <https://github.com/metamath/set.mm/pull/925> (whatever we choose to name
> it). It is not a particularly hard task, just a bit long and a bit boring
> as explained by Benoît. This is typically the kind of task that could be
> easily automated.
>
Thanks a lot !
> h1::subarea.1 |- A e. dom area
>
> h2::subarea.2 |- ( x e. dom A -> C C_ RR )
> h3::subarea.3 |- B = { <. x , y >. | ( <. x , y >. e. A /\ y e. C ) }
> !qed:: |- B e. dom area
>
> It looks false: what if C is not measurable ? (e.g. take A to be the unit
square and C a non-measurable subset of [0,1])
> Also, why not try directly with the deduction version this time? ;-)
>
Indeed !
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/39ecf21c-19db-49b5-8ddb-e952c8644615%40googlegroups.com.
