A Missing Lemma Dual to nn_integral_FTC_atLeast

[伊藤洋介]

👍

伊藤洋介 さんが Gmail
<https://www.google.com/gmail/about/?utm_source=gmail-in-product&utm_medium=et&utm_campaign=emojireactionemail#app>
でリアクションしました

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

> It took a little work to find the right lemmas. But it's worth having
> these lemmas in the long run.
>
> > On 14 Feb 2026, at 12:12, 伊藤洋介 <glacier345 at gmail.com> wrote:
> >
> > 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 --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/vnd.google.email-reaction+json
Size: 37 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260214/67719c34/attachment.bin>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260214/67719c34/attachment.htm>