Homotopy Type Theory
pointwise continuous function > history (Rev #13)
Contents
Definition in cohesive homotopy type theory
In real numbers
Let ℝ \mathbb{R} be the (two-sided) Dedekind real numbers with a term
p ℝ : isContr ( esh ( ℝ ) ) p_\mathbb{R}:isContr(\esh(\mathbb{R}))
representing that the shape of ℝ \mathbb{R} is contractible . and let I I be a closed interval or open interval in ℝ \mathbb{R} . Because the shape of ℝ \mathbb{R} is contractible, the shape of any closed or open interval in ℝ \mathbb{R} is contractible. Given a mapping f : I → ℝ f:I \to \mathbb{R} , let us define the graph G G of the mapping f f as
G ≔ ∑ x : I ( x , f ( x ) ) G \coloneqq \sum_{x:I} (x, f(x))
in the product type I × ℝ I \times \mathbb{R} . f f is continuous if the shape of G G is contractible:
p : isContr ( esh ( G ) ) p:isContr(\esh(G))
Between geometrically contractible spaces
Let S S and T T be space? s with terms
p S : isContr ( esh ( S ) ) p_S:isContr(\esh(S)) p T : isContr ( esh ( T ) ) p_T:isContr(\esh(T))
representing that the shape s of S S and T T are contractible . Given a mapping f : S → T f:S \to T , let us define the graph G G of the mapping f f as
G ≔ ∑ x : S ( x , f ( x ) ) G \coloneqq \sum_{x:S} (x, f(x))
in the product type I × ℝ I \times \mathbb{R} . f f is continuous if the shape of G G is contractible:
p : isContr ( esh ( G ) ) p:isContr(\esh(G))
Definition in homotopy type theory
In rational numbers
Let ℚ \mathbb{Q} be the rational numbers . An function f : ℚ → ℚ f:\mathbb{Q} \to \mathbb{Q} is continuous at a point c : ℚ c:\mathbb{Q}
isContinuousAt ( f , c ) ≔ ∏ ϵ : ℚ + ∏ x : ℚ ‖ ∑ δ : ℚ + ( | x − c | < δ ) → ( | f ( x ) − f ( c ) | < ϵ ) ‖ isContinuousAt(f, c) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \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 f is pointwise continuous in ℚ \mathbb{Q} if it is continuous at all points c c :
isPointwiseContinuous ( f ) ≔ ∏ c : ℚ isContinuousAt ( f , c ) isPointwiseContinuous(f) \coloneqq \prod_{c:\mathbb{Q}} isContinuousAt(f, c)
f f is uniformly continuous in ℚ \mathbb{Q} if
isUniformlyContinuous ( f ) ≔ ∏ ϵ : ℚ + ‖ ∑ δ : ℚ + ∏ x : ℚ ∏ y : ℚ ( x ∼ δ y ) → ( f ( x ) ∼ ϵ f ( y ) ) ‖ isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{\delta:\mathbb{Q}_{+}} \prod_{x:\mathbb{Q}} \prod_{y:\mathbb{Q}} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert
In Archimedean ordered fields
Let F F be an Archimedean ordered field . An function f : F → F f:F \to F is continuous at a point c : F c:F
isContinuousAt ( f , c ) ≔ ∏ ϵ : F + ∏ x : F ‖ ∑ δ : F + ( | x − c | < δ ) → ( | f ( x ) − f ( c ) | < ϵ ) ‖ isContinuousAt(f, c) \coloneqq \prod_{\epsilon:F_{+}} \prod_{x:F} \Vert \sum_{\delta:F_{+}} (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon) \Vert
f f is pointwise continuous in F F if it is continuous at all points c c :
isPointwiseContinuous ( f ) ≔ ∏ c : F isContinuousAt ( f , c ) isPointwiseContinuous(f) \coloneqq \prod_{c:F} isContinuousAt(f, c)
f f is uniformly continuous in F F if
isUniformlyContinuous ( f ) ≔ ∏ ϵ : F + ‖ ∑ δ : F + ∏ x : F ∏ y : F ( x ∼ δ y ) → ( f ( x ) ∼ ϵ f ( y ) ) ‖ isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:F_{+}} \Vert \sum_{\delta:F_{+}} \prod_{x:F} \prod_{y:F} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert
Most general definition
Let S S be a type with a predicate → S \to_S between the type of all nets in S S
∑ I : 𝒰 isDirected ( I ) × ( I → S ) \sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)
and S S itself, and let T T be a type with a predicate → T \to_T between the type of all nets in T T
∑ I : 𝒰 isDirected ( I ) × ( I → T ) \sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)
and T T itself.
A function f : S → T f:S \to T is continuous at a point c : S c:S
isContinuousAt ( f , c ) ≔ ∑ I : 𝒰 isDirected ( I ) × ∏ x : I → S ( x → S c ) → ( f ∘ x → T f ( c ) ) 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))
f f is pointwise continuous if it is continuous at all points c c :
isPointwiseContinuous ( f ) ≔ ∏ c : S isContinuousAt ( f , c ) isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)
See also
Revision on April 2, 2022 at 18:22:11 by
Anonymous? .
See the history of this page for a list of all contributions to it.