UniformContinuous.add
theorem UniformContinuous.add :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α]
[inst_3 : UniformSpace β] {f g : β → α},
UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x + g x
The theorem `UniformContinuous.add` states that for any two functions `f` and `g` mapping from a type `β` to a type `α`, if both `f` and `g` are uniformly continuous and `α` is an add group equipped with a uniform add group structure, then the function that sends each element `x` of `β` to `f x + g x` in `α` is also uniformly continuous. In other words, the theorem asserts that the sum of two uniformly continuous functions is also uniformly continuous when the codomain is a uniform add group.
More concisely: The sum of two uniformly continuous functions from type `β` to an add group `α` is uniformly continuous.
|
UniformContinuous.div
theorem UniformContinuous.div :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α]
[inst_3 : UniformSpace β] {f g : β → α},
UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x / g x
The theorem `UniformContinuous.div` states that for any two types `α` and `β`, where `α` has structure of a uniform space and a group (with the group operation respecting the uniform structure), and `β` is a uniform space, if we have two functions `f` and `g` from `β` to `α` that are uniformly continuous, then the function defined as the quotient of `f` and `g` (i.e., `(f x) / (g x)`) is also uniformly continuous. In other words, if `f` and `g` remain close when their inputs are close, then the same is true for the function which divides `f` by `g` at each point.
More concisely: If `f` and `g` are uniformly continuous functions from a uniform space `β` to a uniform space `α` with `α` being a group, then the quotient function `x ↔− f(x) / g(x)` is also uniformly continuous.
|
uniformContinuous_of_continuousAt_one
theorem uniformContinuous_of_continuousAt_one :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α]
{hom : Type u_3} [inst_3 : UniformSpace β] [inst_4 : Group β] [inst_5 : UniformGroup β] [inst_6 : FunLike hom α β]
[inst_7 : MonoidHomClass hom α β] (f : hom), ContinuousAt (⇑f) 1 → UniformContinuous ⇑f
The theorem `uniformContinuous_of_continuousAt_one` states that for any two uniform groups `α` and `β`, a group homomorphism between them is uniformly continuous if it is continuous at the identity element. This means that the morphism maintains a consistent distance between close elements in the domain and their images under the morphism in the target, regardless of their position in the groups, as long as the morphism is continuous at the identity element. This theorem is a concrete application of uniform continuity in the context of group theory.
More concisely: A group homomorphism between uniform groups is uniformly continuous if it is continuous at the identity element.
|
comm_topologicalAddGroup_is_uniform
theorem comm_topologicalAddGroup_is_uniform :
∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G],
UniformAddGroup G
This theorem states that for any type `G` which is an additive commutative group and has a topological space structure and a topological additive group structure, `G` also has the structure of a uniform additive group. In more mathematical terms, if we have a topological group `G` that is also an Abelian (or commutative) group, then `G` is a uniform additive group. This brings uniform structure to `G`, allowing us to discuss concepts like completeness and uniform continuity in the context of `G`.
More concisely: If `G` is a topological group that is also an Abelian group, then `G` is a uniform additive group.
|
DenseInducing.extend_Z_bilin
theorem DenseInducing.extend_Z_bilin :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [inst : TopologicalSpace α]
[inst_1 : AddCommGroup α] [inst_2 : TopologicalAddGroup α] [inst_3 : TopologicalSpace β] [inst_4 : AddCommGroup β]
[inst_5 : TopologicalSpace γ] [inst_6 : AddCommGroup γ] [inst_7 : TopologicalAddGroup γ]
[inst_8 : TopologicalSpace δ] [inst_9 : AddCommGroup δ] [inst_10 : UniformSpace G] [inst_11 : AddCommGroup G]
[inst_12 : UniformAddGroup G] [inst_13 : T0Space G] [inst_14 : CompleteSpace G] {e : β →+ α}
(de : DenseInducing ⇑e) {f : δ →+ γ} (df : DenseInducing ⇑f) {φ : β →+ δ →+ G},
(Continuous fun p => (φ p.1) p.2) → Continuous (⋯.extend fun p => (φ p.1) p.2)
This theorem, known as the "Bourbaki GT III.6.5 Theorem I", states that for any integer-bilinear continuous functions that map from dense images to a complete Hausdorff group, these functions can be extended by continuity. This is a mathematical concept that means the function can be extended to include points that were not originally in its domain, providing these points are limit points of the original domain. Note that although Bourbaki assumes that α and β are also complete Hausdorff, this theorem does not require such assumption. The parameters α, β, γ, δ, and G represent types with various mathematical structures such as topological spaces, additive commutative groups and uniform spaces. The terms φ, e, and f are additively homomorphic functions with φ being bilinear.
More concisely: Any integer-bilinear, continuous function from a dense subset of a topological space to a complete Hausdorff group can be extended to the whole space.
|
uniformity_eq_comap_nhds_zero
theorem uniformity_eq_comap_nhds_zero :
∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α],
uniformity α = Filter.comap (fun x => x.2 - x.1) (nhds 0)
The theorem `uniformity_eq_comap_nhds_zero` states that for any type `α` that has a uniform space structure, an additive group structure, and is a uniform additive group, the uniformity of `α` is equal to the filter obtained by applying the `comap` function to the difference function `(fun x => x.2 - x.1)` and the neighborhood filter at `0`. In essence, it articulates a connection between the uniformity of the type and the neighborhood of `0` under the operation of subtraction in the context of uniform additive groups.
More concisely: For any uniform additive group α, the uniformity of α is equal to the filter obtained by applying the `comap` function to the difference function and the neighborhood filter at 0.
|
uniformity_eq_comap_nhds_one
theorem uniformity_eq_comap_nhds_one :
∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α],
uniformity α = Filter.comap (fun x => x.2 / x.1) (nhds 1)
This theorem states that for any type `α` that has a `UniformSpace` structure, a `Group` structure, and a `UniformGroup` structure, the uniformity of `α` (which is a filter on the product `α × α` defined by the uniform space structure) is equal to the filter obtained by applying the `comap` function to the function that takes a pair `x` and returns the result of `x.2 / x.1` (where `x.2` and `x.1` represent the second and first elements of the pair `x` respectively), and the neighborhood filter at `1` (which is a filter formed by the set of all neighborhoods of `1`). The `comap` function in this context is used to pull back the neighborhood filter at `1` along the function that divides the second element of a pair by the first one, to get a new filter on `α × α`.
More concisely: For any UniformSpace, Group, and UniformGroup type `α`, the uniformity of `α` equals the pullback of the neighborhood filter at `1` through the function `x mapsto x.2 / x.1`.
|
UniformContinuous.inv
theorem UniformContinuous.inv :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α]
[inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → UniformContinuous fun x => (f x)⁻¹
The theorem `UniformContinuous.inv` states that for any two types `α` and `β`, where `α` is equipped with an instance of `UniformSpace`, `Group`, and `UniformGroup`, and `β` is equipped with an instance of `UniformSpace`, if a function `f` from `β` to `α` is uniformly continuous, then the function that maps `x` in `β` to the inverse of `f(x)` in `α` is also uniformly continuous. In mathematical terms, if `(f x, f y)` tends to the diagonal as `(x, y)` tends to the diagonal, then so does `((f x)⁻¹, (f y)⁻¹)`. This means that if `x` is sufficiently close to `y`, then not only is `f x` close to `f y`, but also the inverse of `f x` is close to the inverse of `f y`, irrespective of where `x` and `y` are located in `β`.
More concisely: If `f: β → α` is uniformly continuous with `α` and `β` being uniform spaces equipped with uniform groups, then the function `x mapsto (f x)⁻¹` is also uniformly continuous.
|
UniformAddGroup.uniformContinuous_iff_open_ker
theorem UniformAddGroup.uniformContinuous_iff_open_ker :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α]
{hom : Type u_3} [inst_3 : UniformSpace β] [inst_4 : DiscreteTopology β] [inst_5 : AddGroup β]
[inst_6 : UniformAddGroup β] [inst_7 : FunLike hom α β] [inst_8 : AddMonoidHomClass hom α β] {f : hom},
UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
This theorem states that for any homomorphism `f` from a uniform additive group `α` to a discrete uniform additive group `β`, `f` is uniformly continuous if and only if the kernel of `f` is an open set in `α`. Here, a uniform additive group is a group equipped with a uniform structure (a kind of topological structure that allows talking about "closeness" of elements) in which the addition operation is uniformly continuous. A homomorphism is a function between two groups that respects the group operations, and the kernel of a homomorphism is the set of all elements in the domain that map to the identity in the codomain. The theorem connects the topological properties of this kernel to the continuity properties of the homomorphism.
More concisely: A homomorphism from a uniform additive group to a discrete uniform additive group is uniformly continuous if and only if the kernel is an open set.
|
uniformContinuous_div
theorem uniformContinuous_div :
∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α],
UniformContinuous fun p => p.1 / p.2
The theorem `uniformContinuous_div` states that for all types `α` which have a Uniform Space structure, a Group structure, and a Uniform Group structure, the function which takes a pair `p` and returns the division of the first element of the pair by the second element of the pair is uniformly continuous. In mathematical terms, this means that for any `α` that forms a uniform group, the division operation is a uniformly continuous function. This implies that no matter where two elements `x` and `y` are located in `α`, if `x` is sufficiently close to `y`, the result of the division `x/y` is close to the result of the division `y/y` (which is 1).
More concisely: For any type `α` with a Uniform Space, Group, and Uniform Group structure, the division function `x ÷ y` on `α` is uniformly continuous.
|
UniformGroup.uniformContinuous_iff_open_ker
theorem UniformGroup.uniformContinuous_iff_open_ker :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α]
{hom : Type u_3} [inst_3 : UniformSpace β] [inst_4 : DiscreteTopology β] [inst_5 : Group β]
[inst_6 : UniformGroup β] [inst_7 : FunLike hom α β] [inst_8 : MonoidHomClass hom α β] {f : hom},
UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
This theorem, `UniformGroup.uniformContinuous_iff_open_ker`, states that for a given homomorphism `f` from a uniform group `α` to a discrete uniform group `β`, it is uniformly continuous if and only if its kernel is open. In detail, the homomorphism is uniformly continuous, which means its output value changes at a rate that does not depend on where you are in the input space `α`, if and only if the pre-image of the identity element under `f` (i.e., the set of all points in `α` that `f` maps to the identity in `β`) is an open set in the topological space of `α`.
More concisely: A homomorphism from a uniform group to a discrete uniform group is uniformly continuous if and only if its kernel is an open set.
|
UniformContinuous.neg
theorem UniformContinuous.neg :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α]
[inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → UniformContinuous fun x => -f x
This theorem states that for any types `α` and `β`, given that `α` is a uniform space, an additive group, and a uniform additive group, and `β` is a uniform space, if a function `f` from `β` to `α` is uniformly continuous, then the function that takes `x` in `β` and maps it to the negative of `f(x)` in `α` is also uniformly continuous. In other words, the negation of a uniformly continuous function is also uniformly continuous.
More concisely: If `f : β -> α` is uniformly continuous between uniform spaces `α` (a uniform space, additive group, and uniform additive group) and `β` (a uniform space), then the function `g : β -> α` defined as `g(x) := -f(x)` is also uniformly continuous.
|
uniformContinuous_add
theorem uniformContinuous_add :
∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α],
UniformContinuous fun p => p.1 + p.2
The theorem `uniformContinuous_add` states that for any type `α` equipped with a uniform space structure, an addition operation, and a uniform addition group structure, the function that takes a pair of elements in `α` and returns their sum is uniformly continuous. In other words, if two pairs of elements in `α` are sufficiently close to each other (in terms of the uniformity structure), then their sums are also close to each other, regardless of the specific location of these pairs in `α`.
More concisely: Given a uniform space `(α, δ)` with addition operation and uniform addition group structure, the addition function is uniformly continuous.
|
uniformContinuous_of_continuousAt_zero
theorem uniformContinuous_of_continuousAt_zero :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α]
{hom : Type u_3} [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : UniformAddGroup β]
[inst_6 : FunLike hom α β] [inst_7 : AddMonoidHomClass hom α β] (f : hom),
ContinuousAt (⇑f) 0 → UniformContinuous ⇑f
The theorem `uniformContinuous_of_continuousAt_zero` states that for any two uniform additive groups `α` and `β`, and any additive group homomorphism `f` (a function that preserves the group operation and belongs to a type that implements `AddMonoidHomClass`) from `α` to `β`, if `f` is continuous at zero, then `f` is uniformly continuous. In other words, if for every sequence in `α` that converges to zero, its image under `f` converges to `f(0)` in `β`, then for any pair of sequences in `α` that converge to each other, their images under `f` also converge to each other, no matter where the sequences are located in `α`.
More concisely: If `f` is an additive group homomorphism from uniform additive group `α` to `β` that is continuous at zero, then `f` is uniformly continuous.
|
uniformContinuous_addMonoidHom_of_continuous
theorem uniformContinuous_addMonoidHom_of_continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α]
{hom : Type u_3} [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : UniformAddGroup β]
[inst_6 : FunLike hom α β] [inst_7 : AddMonoidHomClass hom α β] {f : hom}, Continuous ⇑f → UniformContinuous ⇑f
This theorem states that for any two types `α` and `β`, under certain conditions, if a function `f` of type `hom` (which is a functional-like type from `α` to `β` and is also an additive monoid homomorphism) is continuous, then it is uniformly continuous.
The conditions are that `α` and `β` should have uniform spaces and additive group structures, and these additive groups are also uniform (i.e., they are uniform additive groups). Moreover, the type `hom` should be function-like from `α` to `β` and should be a class of additive monoid homomorphisms from `α` to `β`.
Uniform continuity is a stronger version of continuity that ensures that the function behaves well with respect to the uniformity structure on the types, i.e., if two elements of `α` are close, their images under `f` in `β` are also close. This theorem is particularly useful in the context of topological algebra and analysis.
More concisely: Given types `α` and `β` with uniform structures and additive group structures that are uniform additive groups, if `f` is a continuous, function-like homomorphism from `α` to `β` of type `hom`, then `f` is uniformly continuous.
|
uniformContinuous_mul
theorem uniformContinuous_mul :
∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α],
UniformContinuous fun p => p.1 * p.2
The theorem `uniformContinuous_mul` states that for any type `α` that has a uniform space structure, a group structure, and a uniform group structure, the multiplication operation is uniformly continuous. In other words, if two pairs of elements from `α` are arbitrarily close to each other, then their products are also arbitrarily close to each other, regardless of their actual location in `α`.
More concisely: For any uniform, grouped type `α`, the multiplication operation is uniformly continuous.
|
UniformContinuous.sub
theorem UniformContinuous.sub :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α]
[inst_3 : UniformSpace β] {f g : β → α},
UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x - g x
The theorem `UniformContinuous.sub` states that for any two types, `α` and `β`, where `α` is a uniform space and an additive group (also a uniform additive group), and `β` is a uniform space, given two functions `f` and `g` that map elements from `β` to `α` and are uniformly continuous, the function that maps each element `x` in `β` to the difference of the image of `x` under `f` and `g` (i.e., `f(x) - g(x)`) is also uniformly continuous. This refers to the property that the rate of change (in terms of uniform distance) is constant across the entire domain, regardless of the specific input value.
More concisely: Given uniformly continuous functions `f` and `g` from a uniform space `β` to an additive group and uniform space `α`, their difference `x ↦ f(x) - g(x)` is also uniformly continuous on `β`.
|
uniformContinuous_sub
theorem uniformContinuous_sub :
∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α],
UniformContinuous fun p => p.1 - p.2
The theorem `uniformContinuous_sub` states that for all types `α` that have a uniform space structure, an additive group structure, and a uniform additive group structure, the function that takes a pair of elements of `α` and subtracts the second element from the first is uniformly continuous. In other words, if `x` and `y` are sufficiently close in the uniform space `α`, then the difference `x - y` also approaches zero, regardless of the specific location of `x` and `y` in `α`.
More concisely: For any uniform space `α` equipped with an additive group and a uniform additive group structure, the function subtracting the second element from the first is a uniformly continuous additive homomorphism.
|
UniformContinuous.mul
theorem UniformContinuous.mul :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [inst_2 : UniformGroup α]
[inst_3 : UniformSpace β] {f g : β → α},
UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x * g x
The theorem `UniformContinuous.mul` states that for any two types `α` and `β`, where `α` is equipped with a uniform space structure and a group structure such that it is a uniform group, and `β` is equipped with a uniform space structure, if `f` and `g` are two uniformly continuous functions from `β` to `α`, then the function which maps each element `x` in `β` to the product of `f x` and `g x` in `α` is also uniformly continuous. This means that if `f` and `g` both ensure that close inputs lead to close outputs, then the same property holds for the function defined by their pointwise multiplication.
More concisely: If `f` and `g` are two uniformly continuous functions from a uniform group `β` to a uniform group `α` equipped with a group structure, then their pointwise product is also uniformly continuous.
|