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

Showing changes from revision #8 to #9: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In rational numbers
- In premetric spaces
See also

Definition

In rational numbers

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

isContinuousAt (f, c) ≔ \prod_{ϵ : ℚ_{+}} \prod_{x : I ℚ} ‖ \sum_{δ : ℚ_{+}} (| x - c | < δ) \to (| f (x) - f (c) | < ϵ) ‖

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

$f$ is pointwise continuous in $I ℚ$ I \mathbb{Q} if it is continuous at all points $c$ :

isPointwiseContinuous (f) ≔ \prod_{c : I ℚ} isContinuousAt (f, c)

isPointwiseContinuous(f) \coloneqq ~~\prod_{c:I}~~ \prod_{c:\mathbb{Q}} isContinuousAt(f, c)

$f$ is uniformly continuous in $I ℚ$ I \mathbb{Q} if

isUniformlyContinuous (f) ≔ \prod_{ϵ : ℚ_{+}} ‖ \sum_{δ : ℚ_{+}} \prod_{x : I ℚ} \prod_{y : I ℚ} (x \sim_{δ} y) \to (f (x) \sim_{ϵ} f (y)) ‖

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

In premetric spaces

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ . Let $S$ and $T$ be $R_{+}$ -premetric spaces. A function $f:S \to T$ is continuous at a point $c:S$ ~~if the~~ ~~limit~~ of ~~$f$~~ ~~approaching~~ ~~$c$~~ ~~exists and is equal to~~ ~~$f(c)$~~

isContinuousAt (f, c) ≔ isContr \prod_{ϵ : R_{+}} \prod_{x : S} ‖ \sum_{δ : R_{+}} (\lim_{x \to c} x \sim_{δ} c) \to (f (x) = \sim_{ϵ} f (c)) ‖

isContinuousAt(f, c) \coloneqq ~~isContr(\lim_{x~~ \prod_{\epsilon:R_{+}} \prod_{x:S} \Vert \sum_{\delta:R_{+}} (x \sim_\delta c) \to c} (f(x) ~~f(x)~~ \sim_\epsilon = f(c)) \Vert

$f$ is pointwise continuous if it is continuous at all points $c$ :

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

$f$ is uniformly continuous if

isUniformlyContinuous (f) ≔ \prod_{ϵ : V R_{+}} ‖ \sum_{δ : T R_{+}} \prod_{x : S} \prod_{y : S} (x \sim_{δ} y) \to (f (x) \sim_{ϵ} f (y)) ‖

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

Most general definition

Let $S$ be a type with a predicate $\to_S$ between the type of all nets in $S$

\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

and $S$ itself, and let $T$ be a type with a predicate $\to_T$ between the type of all nets in $T$

\sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)

and $T$ itself.

A function $f:S \to T$ is continuous at a point $c:S$

isContinuousAt(f, c) \coloneqq \sum_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} (x \to_S c) \to (f \circ x \to_T f(c))