tendsto_add
theorem tendsto_add :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M] {a b : M},
Filter.Tendsto (fun p => p.1 + p.2) (nhds (a, b)) (nhds (a + b))
The theorem `tendsto_add` states that for any type `M` that has a topology, an addition operation, and where this addition is continuous, the function that takes a pair of elements `(p.1, p.2)` and returns their sum `p.1 + p.2` is a function that tends to the limit. More explicitly, it states that for any pair of points `(a, b)` in `M`, the sum function tends to the sum `a + b` when the pair of inputs tend to `(a, b)`. In other words, the function 'follows' the topology's sense of closeness: as the inputs get arbitrarily close to `(a, b)`, their sum gets arbitrarily close to `a + b`. This is essentially the definition of a continuous function in terms of filters and topological spaces.
More concisely: Given a type `M` with a topology, an addition operation, and a continuous addition function, the sum function is continuous with respect to this topology.
|
continuous_finset_sum
theorem continuous_finset_sum :
∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
[inst_2 : AddCommMonoid M] [inst_3 : ContinuousAdd M] {f : ι → X → M} (s : Finset ι),
(∀ i ∈ s, Continuous (f i)) → Continuous fun a => s.sum fun i => f i a
This theorem states that for any type `ι`, type `M` and type `X` where `M` has an addition operation and a topology, `X` has a topology, and we have a function `f : ι → X → M`. Given a finite set `s` of `ι`, if for every element `i` in `s`, the function `f(i)` is continuous, then the function that maps every `a` in `X` to the sum (over the set `s`) of `f(i)(a)` is also continuous. This essentially says that the sum of a finite number of continuous functions, where the sum is defined in the way given by the `Finset.sum` definition, is also a continuous function.
More concisely: Given types `ι`, `M` with an addition operation and a topology, and `X` with a topology, if for every `i` in `ι` and `x` in `X`, the function `f(i) : X → M` is continuous, then the function `∫ i in s, f i` defined as the sum `(Finset.sum s) (λ i, f i)`, is also continuous.
|
Filter.Tendsto.mul
theorem Filter.Tendsto.mul :
∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M]
{f g : α → M} {x : Filter α} {a b : M},
Filter.Tendsto f x (nhds a) →
Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => f x * g x) x (nhds (a * b))
The theorem `Filter.Tendsto.mul` states that for any given type `α`, type `M` (which is assumed to be a topological space with a multiplication operation and continuous multiplication), functions `f` and `g` from `α` to `M`, filter `x` on `α`, and elements `a` and `b` of `M`, if the function `f` tends towards the neighborhood of `a` under the filter `x` and the function `g` tends towards the neighborhood of `b` under the same filter `x`, then the function that maps `x` to the product of `f(x)` and `g(x)` tends towards the neighborhood of the product `a * b` under the filter `x`. This theorem is basically asserting the continuity of multiplication in a topological space.
More concisely: Given topological spaces `α` with continuous multiplication `M`, if functions `f` and `g` from `α` to `M` tend to `a` and `b` respectively under filter `x`, then their product function `x mapsto f x * g x` tends to `a * b` under filter `x`.
|
continuous_mul_right
theorem continuous_mul_right :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M] (a : M),
Continuous fun b => b * a
This theorem states that for any type 'M' equipped with a topological space structure, a multiplication operation, and a continuous multiplication operation, multiplication from the right by a fixed element 'a' from 'M' is a continuous function. In other words, given any element 'a' in 'M', the function that multiplies each element 'b' in 'M' by 'a' (from the right) preserves the topological structure; i.e., the preimage of any open set in 'M' under this function is also an open set in 'M'.
More concisely: For any topological space '(M, τ)' equipped with a multiplication operation and a continuous multiplication function, right multiplication by a fixed element 'a' in 'M' is a continuous function.
|
continuous_finset_prod
theorem continuous_finset_prod :
∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
[inst_2 : CommMonoid M] [inst_3 : ContinuousMul M] {f : ι → X → M} (s : Finset ι),
(∀ i ∈ s, Continuous (f i)) → Continuous fun a => s.prod fun i => f i a
This theorem states that for any types `ι`, `M`, and `X`, when `X` and `M` have topological space structures, `M` has a commutative monoid structure, and multiplication on `M` is continuous, if we have a function `f` from type `ι` and `X` to `M` and a finite set `s` of elements of type `ι`, if for every element `i` in `s`, the function `f i` is continuous, then the function which takes an element `a` and sends it to the product over all `i` in `s` of `f i a` is also continuous. In mathematical terms, if $(f_i:X \rightarrow M)$ are continuous functions for all $i$ in a finite set, then the function $a \mapsto \prod_{i \in s} f_i(a)$ is also continuous.
More concisely: If `f:` ι × X → M is a continuous function whose components are all continuous functions from X to a commutative monoid M with continuous multiplication, then the function sending x to ∏i in s (fi x) is continuous.
|
Inducing.continuousAdd
theorem Inducing.continuousAdd :
∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
[inst_3 : AddHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N]
[inst_6 : ContinuousAdd N] (f : F), Inducing ⇑f → ContinuousAdd M
The theorem `Inducing.continuousAdd` states that for any types `M`, `N`, and `F`, given that `M` and `N` are equipped with addition operations, `F` is a function-like object from `M` to `N`, `F` is also an additive homomorphism between `M` and `N`, `M` and `N` are both topological spaces, and `N` supports continuous addition, then for any object `f` of type `F` that induces the topology of `M` from `N`, it follows that `M` also supports continuous addition. In other words, the `Inducing.continuousAdd` theorem captures the idea that if we have a function that is both a homomorphism and induces the topology of its domain from its codomain, and if addition is continuous in the codomain, then addition is also continuous in the domain.
More concisely: If `F` is a continuous, additive homomorphism from a topological space `M` to another topological space `N` with continuous addition, then `M` also has continuous addition.
|
ContinuousOn.mul
theorem ContinuousOn.mul :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Mul M]
[inst_3 : ContinuousMul M] {f g : X → M} {s : Set X},
ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => f x * g x) s
The theorem `ContinuousOn.mul` states that given two topological spaces `X` and `M`, a multiplication operation on `M` which is continuous, and two functions `f` and `g` from `X` to `M` that are continuous on a subset `s` of `X`, then the function that maps each element `x` in `s` to the product of `f(x)` and `g(x)` is also continuous on `s`. This theorem is essentially stating that the multiplication of two continuous functions on a set is also continuous on that set.
More concisely: If two continuous functions map a subset of a topological space to a multiplicatively-associative topological group, then their product is also a continuous function on that subset.
|
tendsto_list_sum
theorem tendsto_list_sum :
∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M]
[inst_2 : ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι),
(∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) →
Filter.Tendsto (fun b => (List.map (fun c => f c b) l).sum) x (nhds (List.map a l).sum)
The theorem `tendsto_list_sum` states that for any list `l` of elements of type `ι`, if for each element `i` in `l`, the function `f` applied to `i` tends towards a neighborhood of `a i` as a filter `x` evolves, then the function which maps `b` to the sum of `f` applied to each element of `l` (i.e., `List.sum (List.map (fun c => f c b) l)`) also tends towards a neighborhood of the sum of `a` applied to each element of `l` (i.e., `List.sum (List.map a l)`) as the same filter `x` evolves. Here, `M` is a type equipped with a topological space structure and an addition operation that is continuous. In simpler terms, this theorem establishes the continuity of the sum of a list of continuous functions in a topological monoid.
More concisely: If each function in a list maps a filter to a neighborhood of a sequence, then the sum function of the list of functions maps the same filter to a neighborhood of the sum of the corresponding sequence values.
|
Filter.Tendsto.add
theorem Filter.Tendsto.add :
∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M]
{f g : α → M} {x : Filter α} {a b : M},
Filter.Tendsto f x (nhds a) →
Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => f x + g x) x (nhds (a + b))
This theorem states that for a topological space `M` with a defined addition operation and equipped with continuous addition, if two functions `f` and `g` from an arbitrary set `α` to `M` respectively tend to points `a` and `b` (in the sense that for any neighborhood of `a` or `b`, the preimage of this neighborhood under `f` or `g` creates a set that "filters" the values of `α`), then the function representing the sum of `f` and `g` tends to the sum of `a` and `b`. In mathematical terms, this theorem establishes the limit law for addition: if $\lim_{x \to c} f(x) = a$ and $\lim_{x \to c} g(x) = b$ then $\lim_{x \to c} (f(x) + g(x)) = a + b$.
More concisely: If `f` and `g` are continuous functions from a set `α` to a topological space `M` with defined addition and equipped with continuous addition, and `a` and `b` are limits of `f(x)` and `g(x)`, respectively, as `x` approaches a limit point `c` in `α`, then the limit of `(f(x) + g(x))` as `x` approaches `c` is equal to `(a + b)`.
|
Filter.tendsto_cocompact_mul_right
theorem Filter.tendsto_cocompact_mul_right :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : ContinuousMul M] {a b : M},
a * b = 1 → Filter.Tendsto (fun x => x * a) (Filter.cocompact M) (Filter.cocompact M)
The theorem `Filter.tendsto_cocompact_mul_right` states that for any topological monoid `M` with continuous multiplication, and any elements `a` and `b` in `M` such that `a * b = 1` (meaning `a` is right-invertible with `b` as its right inverse), the function defined by right-multiplication by `a` (i.e., `fun x => x * a`) is a proper map with respect to the "cocompact" filter on `M`. This means that the preimage of any co-compact set (the complement of a compact set) under this function is again a co-compact set. In other words, this function preserves the property of being co-compact under inverse images.
More concisely: Given a topological monoid with continuous multiplication, if an element is right-inverse to another, then right-multiplication by the former is a proper map with respect to the cocompact filter.
|
continuous_pow
theorem continuous_pow :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : ContinuousMul M] (n : ℕ),
Continuous fun a => a ^ n
This theorem states that for any natural number `n`, the function that raises `a` to the power of `n` is continuous in any topological space `M` that also forms a monoid and supports continuous multiplication. In other words, for any point in the topological space, small changes in the input lead to small changes in the output when we're raising the input to the power `n`.
More concisely: For any natural number `n` and any commutative monoid `M` with a continuous multiplication operation, the power function `x ↦ x ^ n` is continuous on `M`.
|
exists_open_nhds_one_mul_subset
theorem exists_open_nhds_one_mul_subset :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [inst_2 : ContinuousMul M] {U : Set M},
U ∈ nhds 1 → ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
The theorem `exists_open_nhds_one_mul_subset` states that for any topological space `M` that has a multiplication operation and for which multiplication is continuous, if `U` is a neighborhood of the multiplicative identity `1`, then there exists an open set `V` that contains `1` such that the product set `V * V` (i.e., the set of all products of pairs of elements from `V`) is a subset of `U`. This theorem thus involves the concepts of topology, multiplication, and continuous functions, and it's a statement about properties of neighborhoods in the topological space `M`.
More concisely: If `M` is a topological space with a continuous multiplication operation, then for every neighborhood `U` of `1` in `M`, there exists an open set `V` containing `1` such that `V * V` (the set of all products of pairs of elements from `V`) is a subset of `U`.
|
exists_open_nhds_zero_add_subset
theorem exists_open_nhds_zero_add_subset :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [inst_2 : ContinuousAdd M] {U : Set M},
U ∈ nhds 0 → ∃ V, IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U
This theorem states that for any type `M` equipped with a topological space structure, an addition operation, and a continuous addition operation, given an open set `U` that is a neighborhood of `0`, we can find another open set `V` which is also a neighborhood of `0` such that the sum of `V` with itself (i.e., `V + V`) is a subset of `U`.
More concisely: For any topological additive monoid `(M, ℯ, +, 0)`, given an open neighborhood `U` of `0`, there exists an open neighborhood `V` of `0` such that `V + V ⊆ U`.
|
Continuous.pow
theorem Continuous.pow :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
[inst_3 : ContinuousMul M] {f : X → M}, Continuous f → ∀ (n : ℕ), Continuous fun b => f b ^ n
This theorem states that for any types `M` and `X`, where `X` is a topological space and `M` is a topological space with a monoid structure and continuous multiplication, if we have a continuous function `f` from `X` to `M`, then for any natural number `n`, the function defined by taking any element `b` in `X` to the `n`th power of `f(b)` in `M` is also continuous.
More concisely: Given a topological space X, a topological monoid M with continuous multiplication, and a continuous function f : X -> M, the n-th power function g(x) = f(x)^n is also continuous for any natural number n.
|
continuous_mul
theorem continuous_mul :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M],
Continuous fun p => p.1 * p.2
This theorem states that for any type `M` that is a topological space, equipped with a multiplication operation and for which the multiplication operation is continuous, the function that multiplies a pair of elements of `M` is a continuous function. In terms of mathematical language, given a topological space `M` with a continuous multiplication operation, the map `(x, y) ↦ x * y` is a continuous function.
More concisely: If `M` is a topological space equipped with a continuous multiplication operation, then the function `(x, y) mapsto x * y` is a continuous function on `M x M`.
|
continuous_zero
theorem continuous_zero :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Zero M],
Continuous 0
This theorem states that for any two types `M` and `X`, where `X` is a topological space, `M` is a topological space and also has a zero element, the zero function (which assigns the zero element of `M` to every element of `X`) is continuous. In the context of mathematics, a function is continuous if the preimage of every open set is open. Here, the zero function is such that regardless of the input from `X`, the output is always the zero element of `M`.
More concisely: For any topological spaces `X` and `M` with a zero element, the zero function from `X` to `M` is continuous.
|
ContinuousAt.add
theorem ContinuousAt.add :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Add M]
[inst_3 : ContinuousAdd M] {f g : X → M} {x : X},
ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => f x + g x) x
The theorem `ContinuousAt.add` states that for any two functions `f` and `g` from a topological space `X` to another topological space `M` equipped with an addition operation, if both `f` and `g` are continuous at a point `x` in `X`, then their pointwise sum function, which maps each point in `X` to the sum of `f` and `g` evaluated at that point, is also continuous at `x`. Here, continuity of a function at a point is defined as the function's output values tending to the output value at the given point as the inputs tend to that point. This is under the assumption that the addition operation in `M` is continuous.
More concisely: If functions `f` and `g` from topological space `X` to a topologically closed and commutative group `M` with continuous addition are continuous at a point `x` in `X`, then their pointwise sum `f + g` is also continuous at `x`.
|
continuous_nsmul
theorem continuous_nsmul :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : ContinuousAdd M] (n : ℕ),
Continuous fun a => n • a
This theorem states that for any type `M` equipped with a topological space structure, an addition operation that makes `M` an additive monoid, and a continuous addition operation, the function that multiplies an element of `M` by an integer `n` (`n • a`) is continuous.
More concisely: For any topological additive monoid (M, +) with a continuous addition operation, the scalar multiplication function (n => n \\* a) is continuous for all elements a in M and integers n.
|
ContinuousAt.mul
theorem ContinuousAt.mul :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Mul M]
[inst_3 : ContinuousMul M] {f g : X → M} {x : X},
ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => f x * g x) x
The theorem `ContinuousAt.mul` states that given two topological spaces `X` and `M`, where `M` is equipped with a multiplication operation and this operation is continuous, if we have two functions `f` and `g` from `X` to `M` that are continuous at a point `x` in `X`, then the function that assigns to any point `x` the product `f(x) * g(x)` is also continuous at `x`. This is a formalization of the principle that the product of two continuous functions is also continuous.
More concisely: If `M` is a topological space equipped with a continuous multiplication operation, and `f` and `g` are continuous functions from a topological space `X` to `M` at a point `x` in `X`, then their product `f * g` is also continuous at `x`.
|
tendsto_list_prod
theorem tendsto_list_prod :
∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M]
[inst_2 : ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι),
(∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) →
Filter.Tendsto (fun b => (List.map (fun c => f c b) l).prod) x (nhds (List.map a l).prod)
The theorem `tendsto_list_prod` states that for any type `ι`, `α`, and `M` where `M` is a topological space with a monoid structure and continuous multiplication, given a function `f` from `ι` to a function from `α` to `M`, a filter `x` on `α`, and a list `l` of elements of type `ι`, if for all elements `i` in `l`, the function `f i` tends towards the neighborhood of `a i` under the filter `x`, then the function that maps any element `b` of the filter to the product of the list obtained by mapping `f c b` over `l` also tends towards the neighborhood of the product of the list obtained by mapping `a` over `l` under the filter `x`. In other words, it says that the limit of the product of a list of functions is the product of the limits of the functions, provided each function tends to its respective limit.
More concisely: Given a topological space `M` with a monoid structure and continuous multiplication, if for all `i` in a list `l` and for all `x` in a filter on the domain of a function `f` from a type `ι` to functions from an `α` to `M`, `f i(x)` converges to `a i` as `x` approaches a limit, then the function that maps `x` to the product of `f i(x)` over `l` converges to the product of `a i` over `l` as `x` approaches a limit.
|
continuous_add
theorem continuous_add :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M],
Continuous fun p => p.1 + p.2
This theorem states that for any type `M` which has a defined topological space, an addition operation, and satisfies the property of continuous addition, the addition operation `p.1 + p.2` is continuous. In more mathematical terms, if we consider `M` as a topological space and the addition as a binary operation, then the function that takes a pair of elements (`p.1`, `p.2`) and returns their sum is a continuous function in the topological sense.
More concisely: Given a type `M` with a topological space structure, an addition operation, and continuous addition, the addition operation is a continuous function.
|
Filter.Tendsto.pow
theorem Filter.Tendsto.pow :
∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : ContinuousMul M]
{l : Filter α} {f : α → M} {x : M},
Filter.Tendsto f l (nhds x) → ∀ (n : ℕ), Filter.Tendsto (fun x => f x ^ n) l (nhds (x ^ n))
The theorem `Filter.Tendsto.pow` states that for any type `α`, another type `M` which has an underlying topological space structure, a monoid structure, and a structure of continuous multiplication, given a filter `l` on `α`, a function `f` from `α` to `M`, and an element `x` of type `M`, if the function `f` tends to `x` with respect to the filter `l` (meaning, the limit of `f` as `α` approaches `x` is `x`), then for any natural number `n`, the function which sends `x` to the `n`-th power of `f(x)` also tends to the `n`-th power of `x` with respect to the filter `l`. In short, if a function's limit is `x` then the limit of the function's `n`-th power is the `n`-th power of `x`.
More concisely: If a continuous function from a topological space to a monoid with continuous multiplication tends to a point x with respect to a filter, then the function's n-th power also tends to the n-th power of x with respect to that filter.
|
Filter.Tendsto.const_mul
theorem Filter.Tendsto.const_mul :
∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M] (b : M)
{c : M} {f : α → M} {l : Filter α},
Filter.Tendsto (fun k => f k) l (nhds c) → Filter.Tendsto (fun k => b * f k) l (nhds (b * c))
The theorem `Filter.Tendsto.const_mul` states that for any type `α`, any type `M` that is a topological space and has multiplication and continuous multiplication defined on it, a constant `b` of type `M`, a function `f` from `α` to `M`, and a filter `l` on `α`, if the function `f` tends towards a neighborhood of a constant `c` (in the sense that the pre-image under `f` of any neighborhood of `c` is a neighborhood under `l`), then the function which maps `k` to the product of `b` and `f(k)` also tends towards the neighborhood of the product of `b` and `c`. In other words, if a function approaches a certain value in a topological space, then multiplying the function by a constant results in a new function that approaches the product of the constant and the original limit.
More concisely: If a continuous function from a topological space to itself tends to a constant under a filter, then the constant multiplication of the function with another constant tends to the product of the constants.
|
Filter.Tendsto.nsmul
theorem Filter.Tendsto.nsmul :
∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : ContinuousAdd M]
{l : Filter α} {f : α → M} {x : M},
Filter.Tendsto f l (nhds x) → ∀ (n : ℕ), Filter.Tendsto (fun x => n • f x) l (nhds (n • x))
The theorem `Filter.Tendsto.nsmul` states that for any topological space `M` that is also an additive monoid with continuous addition, any filter `l`, any function `f` from `α` to `M`, and any point `x` in `M`, if `f` tends to `x` with respect to `l` (meaning the limit of `f` as it approaches `l` is `x`), then for any natural number `n`, the function that maps `x` to `n` times `f(x)` also tends to `n` times `x` with respect to `l`. In other words, if `f` approaches `x` under filter `l`, then `n * f` approaches `n * x` under the same filter for any natural number `n`, which is a property that shows the compatibility of limit operation with scalar multiplication in this context.
More concisely: If a function `f` tends to a point `x` in a topological monoid `M` with respect to filter `l`, then the function `x => n * f(x)` (scalar multiplication by a natural number `n`) also tends to `n * x` with respect to `l`.
|
Continuous.add
theorem Continuous.add :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Add M]
[inst_3 : ContinuousAdd M] {f g : X → M}, Continuous f → Continuous g → Continuous fun x => f x + g x
This theorem states that if `f` and `g` are both continuous functions from a topological space `X` to another topological space `M` and `M` supports addition operation in a continuous way (expressed by the `ContinuousAdd M` typeclass), then the function that maps each point `x` in `X` to the sum of `f(x)` and `g(x)` in `M` is also a continuous function.
More concisely: If `f` and `g` are continuous functions from a topological space `X` to a topological vector space `M` with continuous addition, then the function `x mapsto f(x) + g(x)` is also continuous.
|
Filter.Tendsto.mul_const
theorem Filter.Tendsto.mul_const :
∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M] (b : M)
{c : M} {f : α → M} {l : Filter α},
Filter.Tendsto (fun k => f k) l (nhds c) → Filter.Tendsto (fun k => f k * b) l (nhds (c * b))
The theorem `Filter.Tendsto.mul_const` states that for any topological space `M` with multiplication operation that is continuous, given any element `b` of `M`, and a filter `l` over some type `α`, if a function `f` from `α` to `M` tends towards a limit `c` as per the neighborhood filter at `c` when applied on `l`, then the function that maps `k` to `f(k) * b` also tends towards the limit `c * b` with respect to the neighborhood filter at `c * b` when applied on `l`. In short, it states that if a function tends towards a limit, then the function multiplied by a constant also tends towards the limit multiplied by the same constant, provided multiplication is continuous in the topological space.
More concisely: If a function from a filter to a topological space with continuous multiplication tends towards a limit, then the function multiplied by a constant tends towards the limit multiplied by that constant.
|
continuous_add_left
theorem continuous_add_left :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M] (a : M),
Continuous fun b => a + b
This theorem states that for any type `M` that has a topological space structure, an addition operation, and where the addition operation is continuous, given any element `a` of type `M`, the function that adds `a` to another element is a continuous function. In mathematical terms, if `(M, +)` is a topological space with continuous addition, then for any `a` in `M`, the map `b ↦ a + b` is continuous.
More concisely: If `(M, +)` is a topological space with continuous addition, then for all `a` in `M`, the function `b mapsto a + b` is a continuous function.
|
Inducing.continuousMul
theorem Inducing.continuousMul :
∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
[inst_3 : MulHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N]
[inst_6 : ContinuousMul N] (f : F), Inducing ⇑f → ContinuousMul M
The theorem `Inducing.continuousMul` states that for any types `M`, `N`, and `F`, if `M` and `N` are equipped with multiplication operations and topological space structures, `F` is a function from `M` to `N` which behaves like a function (due to `FunLike F M N`), and `F` also behaves like a multiplication homomorphism (`MulHomClass F M N`), if multiplication on `N` is continuous (`ContinuousMul N`) and the function `f : F` induces the topology of `M` from `N` (`Inducing ⇑f`), then multiplication on `M` is also continuous (`ContinuousMul M`). In other words, if the multiplication operation is continuous in the codomain of a function that induces the topology and preserves the multiplication operation, then the multiplication operation is also continuous in the domain.
More concisely: If `F : M → N` is a continuous, multiplication-preserving function between topological spaces `M` and `N` with continuous multiplication on `N`, then multiplication is continuous on `M`.
|
Continuous.mul
theorem Continuous.mul :
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Mul M]
[inst_3 : ContinuousMul M] {f g : X → M}, Continuous f → Continuous g → Continuous fun x => f x * g x
This theorem states that for any types `M` and `X`, given that `M` has multiplication defined and is equipped with a topology that makes the multiplication operation continuous, and `X` is also a topological space, if `f` and `g` are both continuous functions from `X` to `M`, then the function that takes an element of `X` and returns the product of `f` and `g` evaluated at that element is also continuous. In other words, the multiplication of two continuous functions is again a continuous function.
More concisely: If `M` is a topological space with continuous multiplication and `X` is also a topological space, then the product of two continuous functions from `X` to `M` is a continuous function.
|
continuous_add_right
theorem continuous_add_right :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M] (a : M),
Continuous fun b => b + a
This theorem states that for any type `M` that has a topological space structure, an addition operation, and for which this addition operation is continuous, the operation of adding a fixed element `a` (of type `M`) to any other element of `M` is a continuous function. In other words, in this framework, right-addition by a fixed element is a continuous operation.
More concisely: For any type `M` with a topological space structure and a continuous addition operation, right-addition by a fixed element is a continuous function.
|
continuous_mul_left
theorem continuous_mul_left :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M] (a : M),
Continuous fun b => a * b
This theorem states that for any type `M` that has a topological space structure, a multiplication operation, and a continuous multiplication operation, multiplying a fixed element `a` of type `M` on the left side with any other element `b` of `M` is a continuous operation. In other words, the map `b ↦ a*b` is continuous in the topology of `M`.
More concisely: For any topological space `M` with a multiplication operation and a continuous multiplication, the left multiplication by a fixed element `a` is a continuous operation.
|
Filter.tendsto_cocompact_mul_left
theorem Filter.tendsto_cocompact_mul_left :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : ContinuousMul M] {a b : M},
b * a = 1 → Filter.Tendsto (fun x => a * x) (Filter.cocompact M) (Filter.cocompact M)
The theorem `Filter.tendsto_cocompact_mul_left` states that for any topological monoid `M` with continuous multiplication, given any two elements `a` and `b` in `M` such that the multiplication of `b` and `a` equals the identity element, the function resulting from left-multiplication by `a` has an interesting property with respect to the filter generated by complements to compact sets in `M`. Specifically, this function tends to map "near" elements (according to the cocompact filter) to "near" elements. In other words, the pre-image under this function of any "neighborhood" (in the sense of the cocompact filter) of an element is again a "neighborhood" of the preimage of that element. This can be seen as a generalization of the property that inverse images of compact sets under a proper map are compact.
More concisely: For any topological monoid with continuous multiplication, left-multiplication by an element with multiplicative inverse mapping the identity is a continuity-preserving function with respect to the filter generated by complements to compact sets.
|
tendsto_mul
theorem tendsto_mul :
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M] {a b : M},
Filter.Tendsto (fun p => p.1 * p.2) (nhds (a, b)) (nhds (a * b))
The theorem `tendsto_mul` states that for any type `M` with a topological space structure, a multiplication operation, and assuming the multiplication operation is continuous, given any two points labelled `a` and `b` in `M`, the limit of the function that takes a pair `p` to the product of the elements of the pair, as the pair `p` approaches `(a, b)` in the topology of `M`, is equal to the product `a * b`. In other words, in a topological space with continuous multiplication, the limit of the multiplication function at any point is just the multiplication of the coordinates of the point.
More concisely: Given a topological space `M` with a continuous multiplication operation, the limit of the function `λp, a * b` as `p` approaches `(a, b)` in the topology of `M` is equal to `a * b`.
|