Homotopy Type Theory
pointwise continuous function > history (Rev #7)
Contents
Definition
In rational numbers
Let ℚ \mathbb{Q} be the rational numbers , and let I I be a closed interval in ℚ \mathbb{Q} . An function f : I → ℚ f:I \to \mathbb{Q} is continuous at a point c : I c:I
isContinuousAt ( f , c ) ≔ ∏ ϵ : ℚ + ∏ x : I ‖ ∑ δ : ℚ + ( | x − c | < δ ) → ( | 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
f f is pointwise continuous in I I if it is continuous at all points c c :
isPointwiseContinuous ( f ) ≔ ∏ c : I isContinuousAt ( f , c ) isPointwiseContinuous(f) \coloneqq \prod_{c:I} isContinuousAt(f, c)
f f is uniformly continuous in I I 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 T T and V V be types, S S be a T T -premetric space and U U be a V V -premetric space . An function f : S → U f:S \to U is continuous at a point c : S c:S if the limit of f f approaching c c exists and is equal to f ( c ) f(c)
isContinuousAt ( f , c ) ≔ isContr ( lim x → c f ( x ) = f ( c ) ) isContinuousAt(f, c) \coloneqq isContr(\lim_{x \to c} f(x) = 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)
f f 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.