Continuity in topological spaces #
For topological spaces X and Y, a function f : X โ Y and a point x : X,
ContinuousAt f x means f is continuous at x, and global continuity is
Continuous f. There is also a version of continuity PContinuous for
partially defined functions.
Tags #
continuity, continuous function
If f x โ s โ ๐ (f x) for continuous f, then f y โ s near x.
This is essentially Filter.Tendsto.eventually_mem, but infers in more cases when applied.
If a function f tends to somewhere other than ๐ (f x) at x,
then f is not continuous at x
See also interior_preimage_subset_preimage_interior.
See note [comp_of_eq lemmas]
A version of Continuous.tendsto that allows one to specify a simpler form of the limit.
E.g., one can write continuous_exp.tendsto' 0 1 exp_zero.
If a continuous map f maps s to t, then it maps closure s to closure t.
If a continuous map f maps s to a closed set t, then it maps closure s to t.
Function with dense range #
A surjective map has dense range.
The image of a dense set under a continuous map with dense range is a dense set.
If f has dense range and s is an open set in the codomain of f, then the image of the
preimage of s under f is dense in s.
If a continuous map with dense range maps a dense set to a subset of t, then t is a dense
set.
Composition of a continuous map with dense range and a function with dense range has dense range.
Given a function f : X โ Y with dense range and y : Y, returns some x : X.
Instances For
The library contains many lemmas stating that functions/operations are continuous. There are many
ways to formulate the continuity of operations. Some are more convenient than others.
Note: for the most part this note also applies to other properties
(Measurable, Differentiable, ContinuousOn, ...).
The traditional way #
As an example, let's look at addition (+) : M โ M โ M. We can state that this is continuous
in different definitionally equal ways (omitting some typing information)
Continuous (fun p โฆ p.1 + p.2);Continuous (Function.uncurry (+));Continuous โฟ(+). (โฟis notation for recursively uncurrying a function)
However, lemmas with this conclusion are not nice to use in practice because
- They confuse the elaborator. The following example fails, because of limitations in the elaboration process.
variable {M : Type*} [Add M] [TopologicalSpace M] [ContinuousAdd M]
example : Continuous (fun x : M โฆ x + x) :=
continuous_add.comp _
-- This example used to fail, but would be accepted if you wrote is as
-- `continuous_add.comp (continuous_id.prodMk continuous_id :)`.
example : Continuous (fun x : M โฆ x + x) :=
continuous_add.comp (continuous_id.prodMk continuous_id)
- If the operation has more than 2 arguments, they are impractical to use, because in your application the arguments in the domain might be in a different order or associated differently.
The convenient way #
A much more convenient way to write continuity lemmas is like Continuous.add:
Continuous.add {f g : X โ M} (hf : Continuous f) (hg : Continuous g) :
Continuous (f + g)
The conclusion can be Continuous (fun x โฆ f x + g x), which is definitionally equal.
This has the following advantages
- It supports projection notation, so is shorter to write.
Continuous.add _ _is recognized correctly by the elaborator and gives useful new goals.- It works generally, since the domain is a variable.
(Having a domain
Y ร Zwould be less convenient in general.)
As an example for a unary operation, we have Continuous.neg.
Continuous.neg {f : X โ G} (hf : Continuous f) : Continuous (-f)
For unary functions, the elaborator is not confused when applying the traditional lemma
(like continuous_neg), but it's still convenient to have the short version available (compare
hf.neg.neg.neg with continuous_neg.comp <| continuous_neg.comp <| continuous_neg.comp hf).
As a harder example, consider an operation of the following type:
def strans {x : F} (ฮณ ฮณ' : Path x x) (tโ : I) : Path x x
The precise definition is not important, only its type. The correct continuity principle for this operation is something like this:
{f : X โ F} {ฮณ ฮณ' : โ x, Path (f x) (f x)} {tโ s : X โ I}
(hฮณ : Continuous โฟฮณ) (hฮณ' : Continuous โฟฮณ')
(ht : Continuous tโ) (hs : Continuous s) :
Continuous (fun x โฆ strans (ฮณ x) (ฮณ' x) (t x) (s x))
Note that all arguments of strans are indexed over X, even the basepoint x, and the last
argument s that arises since Path x x has a coercion to I โ F. The paths ฮณ and ฮณ' (which
are unary functions from I) become binary functions in the continuity lemma.
Summary #
- Make sure that your continuity lemmas are stated in the most general way, and in a convenient
form. That means that:
- The conclusion has a variable
Xas domain (not something likeY ร Z); - Wherever possible, all point arguments
c : Yare replaced by functionsc : X โ Y; - All
n-ary function arguments are replaced byn+1-ary functions (f : Y โ Zbecomesf : X โ Y โ Z); - All (relevant) arguments have continuity assumptions, and perhaps there are additional assumptions needed to make the operation continuous;
- The function in the conclusion is fully applied.
- The conclusion has a variable
- These remarks are mostly about the format of the conclusion of a continuity lemma.
In assumptions it's fine to state that a function with more than 1 argument is continuous using
โฟorFunction.uncurry.
Functions with discontinuities #
In some cases, you want to work with discontinuous functions, and in certain expressions they are
still continuous. For example, consider the fractional part of a number, Int.fract : โ โ โ.
In this case, you want to add conditions to when a function involving fract is continuous, so you
get something like this: (assumption hf could be weakened, but the important thing is the shape
of the conclusion)
lemma ContinuousOn.comp_fract {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
{f : X โ โ โ Y} {g : X โ โ} (hf : Continuous โฟf) (hg : Continuous g) (h : โ s, f s 0 = f s 1) :
Continuous (fun x โฆ f x (fract (g x)))
With ContinuousAt you can be even more precise about what to prove in case of discontinuities,
see e.g. ContinuousAt.comp_div_cases.
Instances For
Lean's elaborator has trouble elaborating applications of lemmas that state that the composition of
two functions satisfy some property at a point, like ContinuousAt.comp / ContDiffAt.comp and
ContMDiffWithinAt.comp. The reason is that a lemma like this looks like
ContinuousAt g (f x) โ ContinuousAt f x โ ContinuousAt (g โ f) x.
Since Lean's elaborator elaborates the arguments from left-to-right, when you write hg.comp hf,
the elaborator will try to figure out both f and g from the type of hg. It tries to figure
out f just from the point where g is continuous. For example, if hg : ContinuousAt g (a, x)
then the elaborator will assign f to the function Prod.mk a, since in that case f x = (a, x).
This is undesirable in most cases where f is not a variable. There are some ways to work around
this, for example by giving f explicitly, or to force Lean to elaborate hf before elaborating
hg, but this is annoying.
Another better solution is to reformulate composition lemmas to have the following shape
ContinuousAt g y โ ContinuousAt f x โ f x = y โ ContinuousAt (g โ f) x.
This is even useful if the proof of f x = y is rfl.
The reason that this works better is because the type of hg doesn't mention f.
Only after elaborating the two ContinuousAt arguments, Lean will try to unify f x with y,
which is often easy after having chosen the correct functions for f and g.
Here is an example that shows the difference:
example [TopologicalSpace X] [TopologicalSpace Y] {xโ : X} (f : X โ X โ Y)
(hf : ContinuousAt (Function.uncurry f) (xโ, xโ)) :
ContinuousAt (fun x โฆ f x x) xโ :=
-- hf.comp (continuousAt_id.prod continuousAt_id) -- type mismatch
-- hf.comp_of_eq (continuousAt_id.prod continuousAt_id) rfl -- works