Homotopy Type Theory pointwise continuous function > history (Rev #7)

Contents

Definition

In rational numbers

Let \mathbb{Q} be the rational numbers, and let II be a closed interval in \mathbb{Q}. An function f:If:I \to \mathbb{Q} is continuous at a point c:Ic:I

isContinuousAt(f,c) ϵ: + x:I δ: +(|xc|<δ)(|f(x)f(c)|<ϵ)isContinuousAt(f, c) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \prod_{x:I} \Vert \sum_{\delta:\mathbb{Q}_{+}} (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon) \Vert

ff is pointwise continuous in II if it is continuous at all points cc:

isPointwiseContinuous(f) c:IisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:I} isContinuousAt(f, c)

ff is uniformly continuous in II if

isUniformlyContinuous(f) ϵ: + δ: + x:I y:I(x δy)(f(x) ϵf(y))isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{\delta:\mathbb{Q}_{+}} \prod_{x:I} \prod_{y:I} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert

In premetric spaces

Let TT and VV be types, SS be a TT-premetric space and UU be a VV-premetric space. An function f:SUf:S \to U is continuous at a point c:Sc:S if the limit of ff approaching cc exists and is equal to f(c)f(c)

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

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)

ff is uniformly continuous if

isUniformlyContinuous(f) ϵ:V δ:T x:S y:S(x δy)(f(x) ϵf(y))isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:V} \Vert \sum_{\delta:T} \prod_{x:S} \prod_{y:S} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert

See also

Revision on March 22, 2022 at 17:04:43 by Anonymous?. See the history of this page for a list of all contributions to it.