A Missing Lemma Dual to nn_integral_FTC_atLeast

[伊藤洋介]

Hello,

Thank you for the reply.
I was surprised since I could not find a proof by symmetry.
I am looking forward to seeing the proof.


2026年2月14日(土) 21:02 Lawrence Paulson <lp15 at cam.ac.uk>:

> Thanks for the suggestion. I did this and I was able to find a proof by
> symmetry, avoiding a near-repetition of the previous proof.
>
> > On 11 Feb 2026, at 12:57, 伊藤洋介 <glacier345 at gmail.com> wrote:
> >
> > Dear Isabelle developers,
> >
> > Could you consider adding the following code to
> Equivalence_Lebesgue_Henstock_Integration.thy?
> > This is the counterpart of the lemma nn_integral_FTC_atLeast.
> >
>
>

-- 
伊藤 洋介
080-5057-6931
glacier345 at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260214/4462b8b0/attachment.htm>