Continuous functions in Isabelle

I want to define a continuous function on an interval of the real line -- [a,b), [a,b], (a,b), or (a,b] (where a < b and either could possibly be infinite) -- in Isabelle, or state that a function is continuous on such an interval.

I believe what I want is continuous_on s f because

"continuous_on s f ⟷ (∀x∈s. (f ⤏ f x) (at x within s))"

(which I got from here:https://isabelle.in.tum.de/library/HOL/HOL/Topological_Spaces.html#Topological_Spaces.topological_space_class.at_within|const)

So I think "s" should be an interval but I'm not sure how best to represent that.

So I would like to know how I could set "s" to any of the types of set intervals I list above. Thank you!

The answer to your question

In every ordered type you can write {a..b} for the closed interval from a to b. For the open/half-open variants there are {a<..b}, {a..<b}, {a<..<b}, {a..}, {..b}, {a<..}, and {..<b}.

These are defined in HOL.Set_Interval and their internal names are things like lessThan, atLeastAtMost, etc.

So in your case, you can simply write something like continuous_on {a..b} f.

It takes some time to understand how to do arguments about limits, continuity, etc. in a theorem prover efficiently. Don't be afraid to ask, either here or on the Zulip. You can of course always do things the hard way (with e.g. ε–δ reasoning) but once you become more proficient in using the library a lot of things become much easier. Which brings me to:

Addendum: Filters

Note however that to really reason about continuity in Isabelle in an idiomatic way you will have to understand filters, which are (among other things) a way to talk about ‘neighbourhoods of points’. There is the definition continuous which takes a function at a filter and can be used to say that a function is continuous at a given point with some conditions.

For instance, there are filters

• nhds x, which describes the neighbourhoods of x (i.e. everything that is sufficiently close to x)
• at x within A, which describes the pointed neighbourhood of x intersected with A – i.e. you approach x without every reaching it and while staying fully inside the set A
• at x, which is simply at x within UNIV, i.e. the pointed neighbourhood of x without further restricitions
• at_left x and at_right x for e.g. the real numbers, which are defined as at x within {..<x} and at x within {x<..}, i.e. the left and right neighbourhoods of x

Then you can write things like continuous (at x) F or continuous (at_right x) F. If I recall correctly, continuous_on A f is equivalent to ∀x∈A. continuous (at x within A) f.

Filters are also useful for many other related things, like limits, open/closed sets, uniform continuity, and derivatives.

This paper explains how filters are used in the Isabelle analysis library. It also has a short section about continuity.