Homotopy Type Theory
pointwise continuous function > history (Rev #9)
Contents
Definition
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 premetric spaces
Let R R be a dense integral subdomain of the rational numbers ℚ \mathbb{Q} and let R + R_{+} be the positive terms of R R . Let S S and T T be R + R_{+} -premetric space s. A function f : S → T f:S \to T is continuous at a point c : S c:S
isContinuousAt ( f , c ) ≔ ∏ ϵ : R + ∏ x : S ‖ ∑ δ : R + ( x ∼ δ c ) → ( f ( x ) ∼ ϵ f ( c ) ) ‖ isContinuousAt(f, c) \coloneqq \prod_{\epsilon:R_{+}} \prod_{x:S} \Vert \sum_{\delta:R_{+}} (x \sim_\delta c) \to (f(x) \sim_\epsilon f(c)) \Vert
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 ) ≔ ∏ ϵ : R + ‖ ∑ δ : R + ∏ x : S ∏ y : S ( x ∼ δ y ) → ( f ( x ) ∼ ϵ f ( y ) ) ‖ isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:R_{+}} \Vert \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 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 March 31, 2022 at 07:05:28 by
Anonymous? .
See the history of this page for a list of all contributions to it.