Homotopy Type Theory
pointwise continuous function > history (Rev #8, changes)
Showing changes from revision #7 to #8:
Added | Removed | Changed
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 R T R and be a dense integral subdomain of the V V rational numbers be types, S ℚ S \mathbb{Q} be and a let T R + T R_{+} - be the positive terms of R R . Let S S and T T be R + R_{+} - premetric space s. and A function U f : S → T U f:S \to T be is 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 31, 2022 at 03:03:47 by
Anonymous? .
See the history of this page for a list of all contributions to it.