ContinuousMap.norm_lt_iff
theorem ContinuousMap.norm_lt_iff :
∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
[inst_2 : NormedAddCommGroup E] (f : C(α, E)) {M : ℝ}, 0 < M → (‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M)
This theorem states that for any topological space `α`, which is also a compact space, and any normed additive commutative group `E`, if we have a continuous map `f` from `α` to `E` and a real number `M` that is greater than zero, then the norm of `f` is less than `M` if and only if the norm of `f` applied to any element `x` in `α` is less than `M`. In simpler terms, the overall norm of a continuous function is less than a positive value if and only if the norm of the function's output is less than that value for every input in the domain.
More concisely: For any compact topological space α and continuous function f from α to a normed additive commutative group E, the function norm ||f|| is less than M if and only if ||f(x)|| < M for all x in α.
|
ContinuousMap.dist_le_two_norm
theorem ContinuousMap.dist_le_two_norm :
∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
[inst_2 : NormedAddCommGroup E] (f : C(α, E)) (x y : α), dist (f x) (f y) ≤ 2 * ‖f‖
This theorem states that for any two points in a compact topological space, the distance between their images under a continuous function into a normed additive commutative group is at most twice the norm of the function. In other words, the distance stretched by the function is bounded by twice its norm.
More concisely: For any compact topological space, the image distance of two points under a continuous function to a normed additive commutative group is less than or equal to twice the norm of the function.
|
ContinuousMap.dist_apply_le_dist
theorem ContinuousMap.dist_apply_le_dist :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : MetricSpace β]
{f g : C(α, β)} (x : α), dist (f x) (g x) ≤ dist f g
This theorem states that for any two continuous functions `f` and `g` from a compact topological space `α` to a metric space `β`, the distance between the functions at any point `x` in `α` is less than or equal to the distance between the functions as a whole. In simpler terms, the pointwise distance between two continuous functions is always controlled or bounded by the overall distance between these two functions.
More concisely: For any compact topological space X, and continuous functions f and g from X to a metric space Y, the pointwise supremum of the distances between f and g is less than or equal to the distance between f and g in the uniform metric on the space of continuous functions from X to Y.
|
ContinuousMap.norm_le
theorem ContinuousMap.norm_le :
∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
[inst_2 : NormedAddCommGroup E] (f : C(α, E)) {C : ℝ}, 0 ≤ C → (‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C)
This theorem states that for any topological compact space `α` and any normed additive commutative group `E`, the norm of a continuous function `f` from `α` to `E` is less than or equal to a non-negative real number `C` if and only if the norm of `f` at every point in `α` is less than or equal to `C`. In other words, the norm of a continuous function is controlled by the upper bound (supremum) of the pointwise norms.
More concisely: A continuous function from a compact topological space to a normed additive commutative group is uniformly continuous, that is, its norm is equal to the supremum of the pointwise norms.
|
ContinuousMap.dist_le
theorem ContinuousMap.dist_le :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : MetricSpace β]
{f g : C(α, β)} {C : ℝ}, 0 ≤ C → (dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C)
The theorem `ContinuousMap.dist_le` states that for two continuous functions `f` and `g` mapping from a compact topological space `α` to a metric space `β`, and for any real number `C` that is greater than or equal to zero, the distance between the two functions `f` and `g` is less than or equal to `C` if and only if the distance between the function values `f(x)` and `g(x)` is less than or equal to `C` for every point `x` in the domain `α`. In other words, the distance between two functions is determined by the largest distance between the function values at any given point.
More concisely: Given compact topological spaces α and metric spaces β, and continuous functions f and g from α to β, the distance between f and g is less than or equal to C if and only if the distance between f(x) and g(x) is less than or equal to C for all x in α.
|
ContinuousMap.norm_coe_le_norm
theorem ContinuousMap.norm_coe_le_norm :
∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
[inst_2 : NormedAddCommGroup E] (f : C(α, E)) (x : α), ‖f x‖ ≤ ‖f‖
This theorem states that for any continuous function `f` from a compact topological space `α` to a normed additively commutative group `E`, the norm of the function applied to any element `x` in `α` is less than or equal to the norm of the function itself. In mathematical terms, for all `f : C(α, E)` and `x : α`, we have `‖f x‖ ≤ ‖f‖`.
More concisely: For any continuous function `f` from a compact topological space `α` to a normed additively commutative group `E`, the norm of `f(x)` is less than or equal to the norm of `f` for all `x` in `α`.
|