Homotopy Type Theory
pointwise continuous function > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
Contents
Definition
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 ) ≔ ∏ ϵ : T V ‖ ∑ δ : V T ∏ x : S ∏ y : S ( x ∼ ϵ δ y ) → ( f ( x ) ∼ δ ϵ f ( y ) ) ‖ isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:T} \prod_{\epsilon:V} \Vert \sum_{\delta:V} \sum_{\delta:T} \prod_{x:S} \prod_{y:S} (x \sim_\epsilon \sim_\delta y) \to (f(x) \sim_\delta \sim_\epsilon f(y)) \Vert
See also
Revision on March 22, 2022 at 13:42:16 by
Anonymous? .
See the history of this page for a list of all contributions to it.