Dear HOL4 and Isabelle community,
the sole purpose of this email is to have your attention on a recent pull
request on HOL4:
https://github.com/HOL-Theorem-Prover/HOL/pull/845
where I was trying to formalize Fubini's theorem (in Lebesgue Integrals)
but was blocked somehow by HOL4's new arithmetic definitions of extended
reals (extreal), i.e. the addition/subtraction of infinities.
In short words, I feel that the statements of this classical result
(Fubini's theorem) by *Guido Fubini* (1879-1943) are not sufficient,
because its proof seems inevitably relied on the forbidden part of extreal
arithmetics. As a result, Fubini's theorem in its original statements has
been or (can be) formalized in Isabelle/HOL, Lean and Mizar, but not in
latest HOL4 where `PosInf + NegInf` is unspecified.
Thanks in advance for your opinions and comments!
Regards,
Chun Tian
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
