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.

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`

.

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?

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