Showing changes from revision #13 to #14:
Added | Removed | Changed
Contents
Definition in cohesive homotopy type theory
Whenever editing is allowed on the nLab again, this article should be ported over there.
In real numbers
Definition
Let be the (two-sided) Dedekind real numbers with a term
In set theory
In Archimedean ordered fields
representing Let that theshape of be anArchimedean ordered field is and letcontractible. and let be a closed interval or open interval in . Because the shape of is contractible, the shape of any closed or open interval in is contractible. Given a mapping , let us define the graph of the mapping as
in be the product positive type elements in . A function is continuous at a point if the shape of is if contractible:
Between geometrically contractible spaces
is pointwise continuous in if it is continuous at all points :
Let and be space?s with terms
is uniformly continuous in if
representing that the shapes of and are contractible. Given a mapping , let us define the graph of the mapping as
In preconvergence spaces
Let and be preconvergence spaces. A function is continuous at a point if
in the product type . is continuous if the shape of is contractible:
is pointwise continuous if it is continuous at all points :
Definition in homotopy type theory
In rational numbers
In homotopy type theory
Let be the rational numbers. An function is continuous at a point
In Archimedean ordered fields
Let be an Archimedean ordered field and let
is pointwise continuous in if it is continuous at all points :
be the positive elements in . A function is continuous at a point
is uniformly continuous in if
is pointwise continuous in if it is continuous at all points :
In Archimedean ordered fields
Let be an Archimedean ordered field. An function is continuous at a point
is uniformly continuous in if
is pointwise continuous in if it is continuous at all points :
In preconvergence spaces
Let and be preconvergence spaces. A function is continuous at a point
is uniformly continuous in if
is pointwise continuous if it is continuous at all points :
Most general definition
Let be a type with a predicate between the type of all nets in
and itself, and let be a type with a predicate between the type of all nets in
and itself.
A function is continuous at a point
is pointwise continuous if it is continuous at all points :
See also