Stream: General

Topic: Limit superior

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 18:39):

Is there a definition for the limit superior operator in one of the sessions distributed with Isabelle? At least for lim sup X ≤ x, I could write something like max X (λ_. x) ⇢ x, but maybe there’s also a dedicated function lim_sup or so.

view this post on Zulip Manuel Eberl (Nov 28 2021 at 19:35):

Yes! There is Limsup :: 'a filter ⇒ ('a ⇒ 'b) ⇒ 'b in HOL-Library.Liminf_Limsup, although it may be better to just import HOL-Analysis.Analysis (and set the session to HOL-Analysis by running JEdit with -l HOL-Analysis) since there may be more useful topological results that are in HOL-Analysis but not in HOL-Library.Liminf_Limsup.

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 20:18):

Thanks a lot for the pointers.

Is HOL-Analysis pre-built, so that I can derive a session from HOL-Analysis instead of HOL, thus saving build time?

view this post on Zulip Lukas Stevens (Nov 28 2021 at 20:19):

Wolfgang Jeltsch said:

Thanks a lot for the pointers.

Is HOL-Analysis pre-built, so that I can derive a session from HOL-Analysis instead of HOL, thus saving build time?

Yes.

Last updated: Jul 15 2022 at 23:21 UTC