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 fromHOL-Analysis
instead ofHOL
, thus saving build time?
Yes.
Last updated: Jul 15 2022 at 23:21 UTC