Homotopy Type Theory pointwise continuous function > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Definition

In premetric spaces

Let TT be a type and SS be a setTT - and aTT-premetric space. An endofunction f:SSf:S \to S is continuous at a point c:Sc:S if the limit of ff approaching cc exists and is equal tof(c)f(c)

isContinuousAt(f,c)isContr(lim xcf(x)=f(c)) isContinuousAt(f, c) \coloneqq \lim_{x isContr(\lim_{x \to c} f(x) = f(c) f(c))

A function ff is pointwise continuous if it is continuous at all points cc:

isPointwiseContinuous(f) c:SisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)

See also

Revision on March 21, 2022 at 03:52:36 by Anonymous?. See the history of this page for a list of all contributions to it.