Homotopy Type Theory
pointwise continuous function > history (Rev #11)
Contents
Definition in cohesive homotopy type theory
Let and be types with terms
representing that the shapes of and are contractible. A function is continuous if the shape of the curve defined by
in the product type is contractible:
Definition in homotopy type theory
In rational numbers
Let be the rational numbers. An function is continuous at a point
is pointwise continuous in if it is continuous at all points :
is uniformly continuous in if
In Archimedean ordered fields
Let be an Archimedean ordered field. An function is continuous at a point
is pointwise continuous in if it is continuous at all points :
is uniformly continuous in if
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
Revision on April 2, 2022 at 02:50:17 by
Anonymous?.
See the history of this page for a list of all contributions to it.