Redirected from "pointwise continuous functions".
Contents
Contents
Idea
The concept of continuous functions familiar from epsilontic analysis.
Definition
Definition
(pointwise continuous function in the real numbers)
Let be the real numbers and let
be the positive elements in . A function is continuous at a point if
is pointwise continuous in if it is continuous at all points :
Definition
(pointwise continuous function between Archimedean ordered fields)
Let and be Archimedean ordered fields and let
be the positive elements in and . A function is continuous at a point if
is pointwise continuous if it is continuous at all points :
Definition
(pointwise continuous function between metric spaces)
Let and be metric spaces, and let
be the positive real numbers. A function is continuous at a point if
is pointwise continuous if it is continuous at all points :
Definition
(pointwise continuous function between preconvergence spaces)
Let and be preconvergence spaces. A function is continuous at a point if
is pointwise continuous if it is continuous at all points :
Definition
(pointwise continuous function in function limit spaces)
Let be a Hausdorff function limit space, and let be a subset of . A function is continuous at a point if the limit of approaching is equal to .
is pointwise continuous on if it is continuous at all points :
As structure
In dependent type theory, one could change the universal quantifiers and existential quantifiers in the definition of uniformly continuous function into dependent product types and dependent sum types.
Definition
Let denote the positive real numbers. Given metric spaces and , a pointwise continuous function between and is a function between their underlying sets with a dependent function which says:
For all elements and for all positive real number , there is as structure a positive real number such that for all elements , is less than whenever is less than
By the type theoretic axiom of choice, which is simply the distributivity of dependent function types over dependent sum types, this is the same as saying that
There exists as structure a function such that for all elements , for all positive real numbers and for all elements , is less than whenever is less than
There exists a similar definition for uniform spaces:
Definition
Given uniform spaces and , a pointwise continuous function between and is a function with a dependent function which says:
For all elements and for all entourages , there is as structure an entourage such that for all elements , whenever
By the type theoretic axiom of choice, which is simply the distributivity of dependent function types over dependent sum types, this is the same as saying that
There exists as structure a function between the sets of entourages such that for all elements and entourages and for all elements , whenever
See also