BoundedContinuousFunction.norm_ofNormedAddCommGroup_le
theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] {f : α → β}
(hfc : Continuous f) {C : ℝ},
0 ≤ C → ∀ (hfC : ∀ (x : α), ‖f x‖ ≤ C), ‖BoundedContinuousFunction.ofNormedAddCommGroup f hfc C hfC‖ ≤ C
This theorem states that for any types `α` and `β`, where `α` is equipped with a Topological Space structure, and `β` is a Semi-normed Additive Commutative Group, any continuous function `f` from `α` to `β` with a positive or zero real number `C` bound such that the norm of `f` at any point `x` in `α` is less than or equal to `C`, then the norm of the bounded continuous function constructed from `f` using `BoundedContinuousFunction.ofNormedAddCommGroup` function is also less than or equal to `C`.
In other words, it ensures that the bounding property `C` of the original function `f` is maintained even after converting the function into a bounded continuous function.
More concisely: For any continuous function from a topological space to a semi-normed additive commutative group with a real number bound, the norm of the bounded continuous function constructed from it is also bounded by the original bound.
|
BoundedContinuousFunction.coe_star
theorem BoundedContinuousFunction.coe_star :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
[inst_2 : StarAddMonoid β] [inst_3 : NormedStarGroup β] (f : BoundedContinuousFunction α β),
⇑(star f) = star ⇑f
This theorem states that for any bounded continuous function 'f' from a topological space 'α' to a semi-normed add commutative group 'β' that also has a structure of a star add monoid and a normed star group, the result of applying the star operation to 'f' and then evaluating the function at a point is the same as first evaluating 'f' at a point and then applying the star operation.
More concisely: For any bounded continuous function $f:\alpha \to (\beta, \star, +, \| \cdot \|)$, where $\beta$ is a semi-normed add commutative group with a structure of a star add monoid and a normed star group, the evaluation of $f\star$ at a point is equal to the application of $\star$ to the evaluation of $f$ at that point: $(f\star)(x) = \star(f(x))$.
|
BoundedContinuousFunction.coe_add
theorem BoundedContinuousFunction.coe_add :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : AddMonoid β]
[inst_3 : LipschitzAdd β] (f g : BoundedContinuousFunction α β), ⇑(f + g) = ⇑f + ⇑g
This theorem states that for any given types `α` and `β`, where `α` is a topological space and `β` is a pseudo metric space with an additive monoid structure and Lipschitz addition, then for any two bounded continuous functions `f` and `g` from `α` to `β`, the application of the sum function `(f + g)` is the same as the sum of the applications of `f` and `g`. In mathematical terms, the definition is `(f + g)(x) = f(x) + g(x)` for all `x` in `α`.
More concisely: For any bounded continuous functions $f$ and $g$ from a topological space $\alpha$ to a pseudo metric space $\beta$ with an additive monoid structure and Lipschitz addition, $(f + g)(x) = f(x) + g(x)$ for all $x$ in $\alpha$.
|
BoundedContinuousFunction.continuous_eval
theorem BoundedContinuousFunction.continuous_eval :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
Continuous fun p => p.1 p.2
This theorem states that the evaluation map, which applies a function `u` to a value `x`, is continuous. This holds for all types `α` and `β`, where `α` is a topological space and `β` is a pseudo metric space. In other words, small changes in the input function or input value result in small changes in the output. The theorem formalizes the intuition that the behavior of functions in these spaces does not suddenly change.
More concisely: The evaluation map, which applies a function from a topological space to a pseudo metric space to an element in the domain, is a continuous function.
|
BoundedContinuousFunction.dist_coe_le_dist
theorem BoundedContinuousFunction.dist_coe_le_dist :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
{f g : BoundedContinuousFunction α β} (x : α), dist (f x) (g x) ≤ dist f g
This theorem states that for any two bounded continuous functions `f` and `g` from a topological space `α` to a pseudo metric space `β`, and for any point `x` in the topological space `α`, the distance between the function values `f(x)` and `g(x)` in the pseudo metric space `β` is always less than or equal to the distance between the functions `f` and `g` themselves. This is essentially expressing that the pointwise distance between the function values is controlled by the overall distance between the functions.
More concisely: For any bounded continuous functions `f` and `g` from a topological space `α` to a pseudo metric space `β` and any `x` in `α`, we have `d(f(x), g(x)) ≤ d(f, g)` in the pseudo metric space `β`, where `d` denotes the distance functions.
|
BoundedContinuousFunction.norm_const_le
theorem BoundedContinuousFunction.norm_const_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (b : β),
‖BoundedContinuousFunction.const α b‖ ≤ ‖b‖
The theorem `BoundedContinuousFunction.norm_const_le` states that for any topological space `α` and any semi-normed additive commutative group `β`, and any member `b` of `β`, the norm of the bounded continuous function that is constantly `b` over `α` is less than or equal to the norm of `b`. Furthermore, if `α` is not an empty set, then the norm of the bounded continuous function is equal to the norm of `b`.
More concisely: For any topological space α, semi-normed additive commutative group β, and constant b in β, the norm of the bounded continuous function from α to β that maps every x in α to b is less than or equal to the norm of b, and is equal to the norm of b if α is non-empty.
|
BoundedContinuousFunction.coe_nsmul
theorem BoundedContinuousFunction.coe_nsmul :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : AddMonoid β]
[inst_3 : LipschitzAdd β] (r : ℕ) (f : BoundedContinuousFunction α β), ⇑(r • f) = r • ⇑f
This theorem states that for any natural number `r` and any bounded continuous function `f` from a topological space `α` to a pseudo metric space `β` (where `β` also has an addition operation that is both a monoid operation and Lipschitz continuous), the function obtained by scaling `f` by `r` is the same as scaling the function `f` first and then applying it. Specifically, if you apply the scaled function to an input, it's the same as multiplying the output of the original function by `r`.
More concisely: For any natural number `r` and a bounded continuous function `f` from a topological space `α` to a pseudo metric space `β` with a Lipschitz continuous addition operation, the function `r * f` equals `f * r` where `r * f(x) = r * f(x)` and `f * r(x) = f(rx)`.
|
Mathlib.Topology.ContinuousFunction.Bounded._auxLemma.8
theorem Mathlib.Topology.ContinuousFunction.Bounded._auxLemma.8 :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), ‖a‖ = dist a 0
This theorem, from the Mathlib library on topology in Lean 4, states that for any type `E` which is a seminormed add group, the norm of an element `a` of `E` is equal to the distance from `a` to the zero element in `E`. This theorem essentially establishes that the norm function `‖a‖` and the distance function `dist a 0` are equivalent in this context. The notation `‖a‖` represents the norm of `a`, and `dist a 0` represents the distance from `a` to `0`.
More concisely: For any seminormed add group `E`, the norm `‖a‖` of an element `a` is equal to the distance `dist a 0` from `a` to the zero element in `E`.
|
BoundedContinuousFunction.coe_neg
theorem BoundedContinuousFunction.coe_neg :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β), ⇑(-f) = -⇑f
This theorem states that for any bounded continuous function `f` from a topological space `α` to a seminormed add commutative group `β`, the negative of `f` (denoted `-f`) operates in the same way as applying the negation to the result of `f`. In other words, negating the function and then applying it to an argument is the same as applying the function to the argument first and then negating the result.
More concisely: For any bounded continuous function `f` from a topological space `α` to a seminormed add commutative group `β`, negating the function `-f` and applying it to an element `x` in `α` is equivalent to applying `f` to `-x` and negating the result.
|
BoundedContinuousFunction.arzela_ascoli
theorem BoundedContinuousFunction.arzela_ascoli :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
[inst_3 : T2Space β] (s : Set β),
IsCompact s →
∀ (A : Set (BoundedContinuousFunction α β)),
(∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) →
(Equicontinuous fun x => ⇑↑x) → IsCompact (closure A)
This theorem, known as the Arzela-Ascoli Theorem, states that for a given set `s` in a pseudometric space `β`, if `s` is compact and we have a set `A` of bounded continuous functions from a compact topological space `α` to `β`, such that for all functions `f` in `A` and for all `x` in `α`, the value `f(x)` is in `s`, and if these functions are equicontinuous (meaning the functions in `A` change uniformly with respect to `x`), then the closure of the set `A` is also compact. This theorem is a fundamental result in analysis and is used in the study of the convergence of sequences of functions.
More concisely: If `α` is a compact topological space, `β` is a pseudometric space, `s ⊆ β` is compact, and `A ⊆ C(α→β)` is a set of bounded, continuous functions such that for all `x ∈ α` and `f, g ∈ A`, `d(f(x), g(x))` is bounded, then the closure of `A` in `C(α→β)` is compact.
|
BoundedContinuousFunction.arzela_ascoli₁
theorem BoundedContinuousFunction.arzela_ascoli₁ :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
[inst_3 : CompactSpace β] (A : Set (BoundedContinuousFunction α β)),
IsClosed A → (Equicontinuous fun x => ⇑↑x) → IsCompact A
The Arzela-Ascoli Theorem, in its first version, states that for a given set `A` of bounded continuous functions mapping from a topological space `α` (which is also a compact space) to a pseudo-metric space `β` (also a compact space), if the set `A` is closed and the functions in `A` are equicontinuous (namely, they change at the same rate at every point in their domain), then `A` itself is compact. In other words, every nontrivial filter that contains `A` has a cluster point in `A`. This theorem provides a crucial link between compactness and equicontinuity in the context of function spaces.
More concisely: Given a set `A` of bounded, continuous functions from a compact space `α` to a compact pseudo-metric space `β`, if `A` is closed and equicontinuous, then `A` is compact.
|
BoundedContinuousFunction.dist_le_iff_of_nonempty
theorem BoundedContinuousFunction.dist_le_iff_of_nonempty :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
{f g : BoundedContinuousFunction α β} {C : ℝ} [inst_2 : Nonempty α],
dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
This theorem states that for any two bounded continuous functions `f` and `g` mapping from a topological space `α` to a pseudometric space `β`, and for any real number `C`, 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 `α`. This holds true given that `α` is nonempty.
More concisely: For any bounded continuous functions `f` and `g` from a nonempty topological space `α` to a pseudometric space `β`, the functions have distance at most `C` if and only if the images `f(x)` and `g(x)` of each point `x` in `α` have distance at most `C`.
|
BoundedContinuousFunction.norm_eq_of_nonempty
theorem BoundedContinuousFunction.norm_eq_of_nonempty :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β) [h : Nonempty α], ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
This theorem states that for any bounded continuous function `f` from a non-empty topological space `α` to a semi-normed addition commutative group `β`, the norm of `f` is equal to the greatest lower bound (or infimum) of the set of all `C` such that the norm of `f(x)` is less than or equal to `C` for all `x` in `α`. This means that we do not need the `0 ≤ C` condition in the formula for `‖f‖` as a `sInf` when the domain is non-empty.
More concisely: The norm of a bounded continuous function from a non-empty topological space to a semi-normed additive commutative group equals the infimum of the norms over all points in the space.
|
BoundedContinuousFunction.continuous_eval_const
theorem BoundedContinuousFunction.continuous_eval_const :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {x : α},
Continuous fun f => f x
This theorem, `BoundedContinuousFunction.continuous_eval_const`, states that for any given point `x` in a topological space `α`, the function that maps each bounded continuous function `f: α → β` to its value at `x` is a continuous function. Here, `β` is assumed to be a pseudo-metric space, which is a generalization of the concept of a metric space.
More concisely: The function that maps each bounded continuous function from a topological space to its value at a point is a continuous function, where the target space is a pseudo-metric space.
|
BoundedContinuousFunction.arzela_ascoli₂
theorem BoundedContinuousFunction.arzela_ascoli₂ :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
(s : Set β),
IsCompact s →
∀ (A : Set (BoundedContinuousFunction α β)),
IsClosed A →
(∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) →
(Equicontinuous fun x => ⇑↑x) → IsCompact A
The Arzelà-Ascoli Theorem (second version) states that for any given topological space `α`, compact space `α`, and pseudometric space `β`, if we have a set `s` that is compact in `β`, and a set `A` of bounded continuous functions from `α` to `β` that is closed, such that for all functions `f` from `A` and all elements `x` in `α`, the value `f(x)` belongs to `s`, and if the family of functions in `A` is equicontinuous at each point of `α`, then the set `A` of these functions is also compact.
More concisely: If a compact subset of a pseudometric space is uniformly inhabited by a closed, equicontinuous set of bounded continuous functions, then that set is compact.
|
BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg
theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg :
∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ),
⇑f = NNReal.toReal ∘ ⇑f.nnrealPart - NNReal.toReal ∘ ⇑(-f).nnrealPart
This theorem states that for any topological space `α` and any bounded continuous function `f` from `α` to the real numbers, the function `f` can be decomposed into the difference of its positive and negative parts. Specifically, the function `f` is equal to the composition of the non-negative real part of `f` and the real number coercion function `NNReal.toReal`, minus the composition of the non-negative real part of the negation of `f` and the real number coercion function `NNReal.toReal`.
More concisely: For any topological space `α` and bounded continuous function `f` from `α` to the real numbers, `f` can be expressed as the difference of its positive part and negative part, i.e., `f = (√abs ∘ f) - (√abs ∘ (-f))`, where `√abs` denotes the non-negative real part function.
|
BoundedContinuousFunction.dist_set_exists
theorem BoundedContinuousFunction.dist_set_exists :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
{f g : BoundedContinuousFunction α β}, ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C
This theorem states that for any two bounded continuous functions `f` and `g`, which map from a topological space `α` to a pseudo metric space `β`, there exists a non-negative real number `C` such that the distance between the images of any point `x` in `α` under functions `f` and `g` (i.e., `f(x)` and `g(x)`) is less than or equal to `C`. In other words, the difference between the outputs of these two functions is always bounded by some constant `C` for all inputs from the topological space `α`.
More concisely: Given any two bounded continuous functions `f` and `g` from a topological space `α` to a pseudo metric space `β`, there exists a constant `C` such that `d(f(x), g(x)) ≤ C` for all `x ∈ α`, where `d` denotes the distance function in `β`.
|
BoundedContinuousFunction.coe_smul
theorem BoundedContinuousFunction.coe_smul :
∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
[inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : BoundedSMul 𝕜 β]
(c : 𝕜) (f : BoundedContinuousFunction α β), ⇑(c • f) = fun x => c • f x
This theorem states that for any types `α`, `β`, and `𝕜`, where `𝕜` is a pseudometric space, `α` is a topological space, and `β` is a pseudometric space with zero and scalar multiplication properties, and where `𝕜` and `β` can be scalars of a bounded scalar multiplication, the function of a scalar `c` multiplied by a bounded continuous function `f` (denoted as `c • f`) applied to an element `x` is equal to the scalar `c` multiplied by the application of `f` to `x` (expressed as `c • f x`). In simpler terms, it describes a property of scalar multiplication in the context of bounded continuous functions.
More concisely: For any bounded continuous function `f` from a topological space `α` to a pseudometric space `β` with scalar multiplication, and for any scalar `c` and point `x` in `α`, the scalar multiplication `c • (f x)` equals the application of `c • f` to `x`.
|
BoundedContinuousFunction.dist_le_two_norm
theorem BoundedContinuousFunction.dist_le_two_norm :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β) (x y : α), dist (f x) (f y) ≤ 2 * ‖f‖
This theorem states that for any two points in a topological space, the distance between their images under a bounded continuous function (which maps to a semi-normed additive commutative group) is at most twice the norm of that function. This provides a constraint on the maximum change in value that can be induced by such a function, given its norm.
More concisely: For any two points in a topological space and a bounded, continuous function to a semi-normed additive commutative group, the image distance is less than or equal to twice the function's norm.
|
BoundedContinuousFunction.continuous_comp
theorem BoundedContinuousFunction.continuous_comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G),
Continuous (BoundedContinuousFunction.comp G H)
The theorem states that for any Lipschitz continuous function `G` with a nonnegative real number constant `C` from a pseudoMetric space `β` to another pseudoMetric space `γ`, and any function from a topological space `α` to `β` that is both bounded and continuous, the composition operator that applies `G` to the output of the bounded continuous function is a continuous operation. This essentially means that if you have a Lipschitz continuous function and a bounded continuous function, composing them in this way retains the continuous property.
More concisely: Given a Lipschitz continuous function `G` with constant `C` from pseudoMetric space `β` to pseudoMetric space `γ`, and a bounded and continuous function `f` from topological space `α` to `β`, the composition `G ∘ f` is a continuous function from `α` to `γ`.
|
BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg
theorem BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg :
∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ),
abs ∘ ⇑f = NNReal.toReal ∘ ⇑f.nnrealPart + NNReal.toReal ∘ ⇑(-f).nnrealPart
This theorem states that for any bounded continuous function `f` from a topological space `α` to the real numbers ℝ, the absolute value of `f` is the sum of the nonnegative real part of `f` and the nonnegative real part of `-f`. In other words, the absolute value of a bounded continuous function can be expressed in terms of its positive and negative components.
More concisely: For any bounded continuous function `f` from a topological space `α` to the real numbers ℝ, |`f`| = (∥f∥^+) + (∥-f∥^+), where ∥⋅∥^+ denotes the nonnegative part of a real number.
|
BoundedContinuousFunction.lipschitz_comp
theorem BoundedContinuousFunction.lipschitz_comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G),
LipschitzWith C (BoundedContinuousFunction.comp G H)
The theorem `BoundedContinuousFunction.lipschitz_comp` states that for any topological space `α` and any two pseudometric spaces `β` and `γ`, if a function `G` from `β` to `γ` is Lipschitz continuous with a nonnegative real number `C` as its Lipschitz constant, then the composition operator (in the target) with `G` is also Lipschitz continuous with the same Lipschitz constant `C`. In other words, if `G` satisfies the property that the distance between its values at any two points in `β` is less than or equal to `C` times the distance between the two points, then the composition of any bounded continuous function with `G` also satisfies this property.
More concisely: If `G : β → γ` is a Lipschitz continuous function from one pseudometric space to another with Lipschitz constant `C`, then the composition of any bounded continuous function from a topological space to `β` with `G` is also Lipschitz continuous with constant `C`.
|
BoundedContinuousFunction.norm_le
theorem BoundedContinuousFunction.norm_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
{f : BoundedContinuousFunction α β} {C : ℝ}, 0 ≤ C → (‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C)
This theorem, `BoundedContinuousFunction.norm_le`, states that for any types `α` and `β`, where `α` is a topological space and `β` is a semi-normed additively commutative group, for any bounded continuous function `f` from `α` to `β` and any real number `C` greater than or equal to zero, the norm of `f` is less than or equal to `C` if and only if the norm of `f` at any point `x` in `α` is less than or equal to `C`. In other words, the norm of a function is controlled by the supremum (greatest value) of the pointwise norms.
More concisely: For any bounded continuous function between a topological space and a semi-normed additively commutative group, the function's norm is equal to the supreme norm of its values at individual points.
|
BoundedContinuousFunction.dist_le
theorem BoundedContinuousFunction.dist_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
{f g : BoundedContinuousFunction α β} {C : ℝ}, 0 ≤ C → (dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C)
This theorem, `BoundedContinuousFunction.dist_le`, states that for any two bounded continuous functions `f` and `g` from a topological space `α` to a pseudo metric space `β`, and any non-negative real number `C`, the distance between `f` and `g` is at most `C` if and only if the distance between `f(x)` and `g(x)` is at most `C` for all `x` in `α`. Here, the distance between two functions is defined as the supremum of the pointwise distances.
More concisely: For bounded continuous functions $f$ and $g$ from a topological space $\alpha$ to a pseudo metric space $\beta$, and real number $C \geq 0$, $ \sup\_{x \in \alpha} d(f(x), g(x)) \leq C $ if and only if $ d(f, g) \leq C $, where $d(f,g)$ is the pointwise supremum distance between $f$ and $g$.
|
BoundedContinuousFunction.dist_le_two_norm'
theorem BoundedContinuousFunction.dist_le_two_norm' :
∀ {β : Type v} {γ : Type w} [inst : SeminormedAddCommGroup β] {f : γ → β} {C : ℝ},
(∀ (x : γ), ‖f x‖ ≤ C) → ∀ (x y : γ), dist (f x) (f y) ≤ 2 * C
This theorem states that for any type `β` which is a seminormed add commutative group and a function `f` from type `γ` to `β`, given a real number `C`, if the norm of `f(x)` is less than or equal to `C` for all `x` of type `γ`, then the distance between `f(x)` and `f(y)` for any `x` and `y` of type `γ` is less than or equal to `2*C`. It essentially establishes a bound on the distance between the image points of any two elements under a function in terms of a constant `C` that bounds the norm of the function.
More concisely: Given a seminormed add commutative group `β` and a function `f` from type `γ` to `β`, if the norm of `f(x)` is bounded by `C` for all `x` in `γ`, then the norm of `f(x) - f(y)` is less than or equal to `2*C` for all `x` and `y` in `γ`.
|
BoundedContinuousFunction.norm_eq_iSup_norm
theorem BoundedContinuousFunction.norm_eq_iSup_norm :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β), ‖f‖ = ⨆ x, ‖f x‖
This theorem states that for any bounded continuous function `f` from a topological space `α` to a semi-normed additive commutative group `β`, the norm of `f` is equal to the supremum of the norms of `f(x)` for all `x` in `α`. In other words, the norm of the function is determined by the largest norm of its values.
More concisely: For any bounded continuous function from a topological space to a semi-normed additive commutative group, the norm of the function equals the supremum of the norms of its values.
|
BoundedContinuousFunction.continuous
theorem BoundedContinuousFunction.continuous :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
(f : BoundedContinuousFunction α β), Continuous ⇑f
This theorem states that for any two types `α` and `β`, where `α` is equipped with a topology and `β` is equipped with a pseudo metric space structure, any bounded continuous function `f` from `α` to `β` is itself continuous. In mathematical terms, if $f$ is a bounded continuous function between a topological space and a pseudometric space, then $f$ is a continuous function.
More concisely: A bounded continuous function between a topological space and a pseudometric space is continuous.
|
BoundedContinuousFunction.uniformContinuous_comp
theorem BoundedContinuousFunction.uniformContinuous_comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G),
UniformContinuous (BoundedContinuousFunction.comp G H)
The theorem `BoundedContinuousFunction.uniformContinuous_comp` states that for any three types `α`, `β`, and `γ` where `α` has a topology and `β` and `γ` have pseudo metric spaces, and for any function `G` from `β` to `γ` with a nonnegative real number `C`, if `G` is Lipschitz continuous with constant `C`, then the function produced by composing `G` (on the target) with any bounded continuous function from `α` to `β` is uniformly continuous. In mathematical terms, if `G : β → γ` is Lipschitz continuous and `f : α → β` is a bounded continuous function, then the composed function `G ∘ f : α → γ` is uniformly continuous. This theorem essentially tells us that composing a bounded continuous function with a Lipschitz continuous function results in a uniformly continuous function.
More concisely: If a Lipschitz continuous function with a constant C composes with a bounded continuous function, the result is a uniformly continuous function.
|
BoundedContinuousFunction.norm_coe_le_norm
theorem BoundedContinuousFunction.norm_coe_le_norm :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β) (x : α), ‖f x‖ ≤ ‖f‖
This theorem states that for any topological space `α` and any seminormed add commutative group `β`, for any bounded continuous function `f` from `α` to `β` and any element `x` in `α`, the norm of the function evaluated at `x` is less than or equal to the norm of the function `f`. In mathematical notation, this is equivalent to saying that for all `f` and `x`, `‖f(x)‖ ≤ ‖f‖`. This theorem is a key property of bounded continuous functions in functional analysis.
More concisely: The norm of a bounded continuous function's evaluation at a point is less than or equal to the function's norm.
|
BoundedContinuousFunction.norm_eq
theorem BoundedContinuousFunction.norm_eq :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β), ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}
This theorem states that the norm of a bounded continuous function is equal to the supremum of the norms of its values. Specifically, for a function `f` from a topological space `α` to a seminormed additive commutative group `β`, the norm of `f` is the least upper bound (`sInf` or supremum) of the set containing all `C` such that `C` is non-negative and the norm of `f(x)` for any `x` in `α` is less than or equal to `C`. The use of `sInf` ensures that the definition works even if `α` has no elements.
More concisely: The norm of a bounded continuous function from a topological space to a seminormed additive commutative group equals the supremum of the norms of its values.
|
BoundedContinuousFunction.isBounded_range
theorem BoundedContinuousFunction.isBounded_range :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
(f : BoundedContinuousFunction α β), Bornology.IsBounded (Set.range ⇑f)
This theorem states that for any bounded continuous function `f` from a topological space `α` to a pseudo metric space `β`, the range of the function `f` (i.e., the set of all its output values) is a bounded set with respect to the bornology of `β`. Here, a set is said to be bounded in a bornology if its complement is co-bounded. The boundedness of a function means that there is a real number such that the absolute differences of the function values are always less than that real number, while a continuous function is one where small changes in the input lead to small changes in the output.
More concisely: For any bounded and continuous function `f` from a topological space `α` to a pseudo metric space `β`, the range of `f` is a bounded set in `β` with respect to its bornology.
|
BoundedContinuousFunction.coe_zero
theorem BoundedContinuousFunction.coe_zero :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β], ⇑0 = 0
This theorem states that for any types `α` and `β`, where `α` is a topological space and `β` is a pseudo metric space with a defined zero, the function that applies the zero constant function (denoted by `0` here) is equivalent to the zero function. In other words, in this particular setting, applying the zero constant to any input yields the zero value of the space.
More concisely: For any topological space `α` and pseudo metric space `β` with defined zero, the constant function `0 : α → β` equals the zero function.
|
BoundedContinuousFunction.inducing_coeFn
theorem BoundedContinuousFunction.inducing_coeFn :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
Inducing (⇑UniformFun.ofFun ∘ DFunLike.coe)
The theorem `BoundedContinuousFunction.inducing_coeFn` states that for any types `α` and `β`, where `α` is a topological space and `β` is a pseudo metric space, the topology on the space of bounded, continuous functions from `α` to `β` (`α →ᵇ β`) is precisely the topology induced by the natural map to the space of uniformly continuous functions from `α` to `β` (`α →ᵤ β`). This natural map is composed of the `UniformFun.ofFun` function, which reinterprets a function from `α` to `β` as an element of `α →ᵤ β`, and the `DFunLike.coe` function, which takes a `DFunLike` object and returns a function from `α` to `β`.
More concisely: The topology on the space of bounded, continuous functions from a topological space `α` to a pseudometric space `β` is equal to the topology induced by the natural map from `α →ᵇ β` to `α →ᵤ β`.
|
BoundedContinuousFunction.ext
theorem BoundedContinuousFunction.ext :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
{f g : BoundedContinuousFunction α β}, (∀ (x : α), f x = g x) → f = g
This theorem states that for any two bounded continuous functions `f` and `g` from a topological space `α` to a pseudo metric space `β`, if for every element `x` in the topological space `α` the value of the functions `f` and `g` are equal, then the functions `f` and `g` are the same. In other words, two bounded continuous functions are identical if they coincide at every point in their domain.
More concisely: If two bounded continuous functions from a topological space to a pseudo metric space are equal at every point, then they are identical.
|
BoundedContinuousFunction.dist_zero_of_empty
theorem BoundedContinuousFunction.dist_zero_of_empty :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
{f g : BoundedContinuousFunction α β} [inst_2 : IsEmpty α], dist f g = 0
This theorem states that for any two bounded continuous functions `f` and `g` mapping from a topological space `α` to a pseudometric space `β`, if the topological space `α` is empty (`IsEmpty α`), then the distance between `f` and `g` is 0. In other words, when the domain is empty, all bounded continuous functions on that domain are considered to have zero distance from each other.
More concisely: For any bounded continuous functions `f` and `g` mapping from an empty topological space `α` to a pseudometric space `β`, the distance between `f` and `g` is 0.
|
BoundedContinuousFunction.nnnorm_le
theorem BoundedContinuousFunction.nnnorm_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β) (C : NNReal), ‖f‖₊ ≤ C ↔ ∀ (x : α), ‖f x‖₊ ≤ C
The theorem `BoundedContinuousFunction.nnnorm_le` states that, given a topological space `α`, a semi-normed additively commutative group `β`, a bounded continuous function `f` from `α` to `β`, and a nonnegative real number `C`, the nonnegative norm (`nnnorm`) of `f` is less than or equal to `C` if and only if the `nnnorm` of `f` evaluated at any point `x` in `α` is less than or equal to `C`. In other words, the norm of a bounded continuous function is controlled by the supremum (greatest value) of the pointwise norms.
More concisely: A bounded continuous function from a topological space to a semi-normed additively commutative group satisfies the property that its supremum (or greatest pointwise value) of the norm equals its own norm if and only if the norm of the function at each point is less than or equal to the supremum.
|
BoundedContinuousFunction.bounded
theorem BoundedContinuousFunction.bounded :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
(f : BoundedContinuousFunction α β), ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
This theorem states that for every bounded continuous function `f` from a topological space `α` to a pseudo metric space `β`, there exists a real number `C` such that the distance between `f(x)` and `f(y)` for any `x` and `y` in `α` is less than or equal to `C`. In other words, the distances between all pairs of values of a bounded continuous function are bounded by some constant.
More concisely: Every bounded continuous function from a topological space to a pseudo metric space has a uniform bound on its values.
|