ContinuousSMul.continuous_smul
theorem ContinuousSMul.continuous_smul :
∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace X]
[self : ContinuousSMul M X], Continuous fun p => p.1 • p.2
This theorem states that the scalar multiplication operation `(•)` is a continuous function. Specifically, for any types `M` and `X` where `M` is a scalar type and `X` is a vector type, and given instances of `M` being a scalar multiplier of `X` (indicated by `[inst : SMul M X]`) and both `M` and `X` have topological space structures, scalar multiplication is continuous. In other words, given a pair `p` consisting of a scalar and a vector, the operation of multiplying the scalar with the vector produces a result that changes continuously with changes in the input pair. This is under the condition that the scalar multiplication operation on the given types `M` and `X` is continuous (`[self : ContinuousSMul M X]`).
More concisely: Given types `M` and `X` with `M` a scalar type, `X` a vector type, instances of `M` being a scalar multiplier of `X` and both having topological space structures, and a continuous scalar multiplication operation, the scalar multiplication function `(•) : M → X → X` is a continuous function.
|
Filter.Tendsto.smul
theorem Filter.Tendsto.smul :
∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : SMul M X] [inst_3 : ContinuousSMul M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X},
Filter.Tendsto f l (nhds c) →
Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x • g x) l (nhds (c • a))
The theorem `Filter.Tendsto.smul` states that if for a topological space `M`, another topological space `X`, a scalar multiplication operation (`SMul`) on `M` and `X`, and a continuity condition (`ContinuousSMul`) for this operation, a filter `l` over a type `α`, a scalar `c` of type `M`, and a point `a` of type `X`, if a function `f` from `α` to `M` tends to `c` through the filter `l` and another function `g` from `α` to `X` tends to `a` through the same filter `l`, then the function defined as the scalar multiplication of `f x` and `g x` for each `x` in `α` tends to the scalar multiplication of `c` and `a` through the same filter `l`. In mathematical terms, if $\lim_{x \to l} f(x) = c$ and $\lim_{x \to l} g(x) = a$, then $\lim_{x \to l} (f(x) \cdot g(x)) = c \cdot a$.
More concisely: If functions $f : \alpha \to M$ and $g : \alpha \to X$ tend to $c \in M$ and $a \in X$, respectively, through filter $l$, then the scalar multiplication $f \cdot g : \alpha \to M \times X$ tends to $(c, a) \in M \times X$ through filter $l$.
|
ContinuousVAdd.continuous_vadd
theorem ContinuousVAdd.continuous_vadd :
∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace X]
[self : ContinuousVAdd M X], Continuous fun p => p.1 +ᵥ p.2
This theorem states that for any types `M` and `X` with `M` having an additive action on `X`, and both `M` and `X` equipped with a topological space structure, if the additive action is continuous (as stated by the `ContinuousVAdd M X` instance), then the function taking a pair `(m, x)` to `m +ᵥ x` is a continuous function. In other words, the operation of "adding" an element of `M` to an element of `X` (via the `+ᵥ` operation) preserves the continuity of the spaces.
More concisely: If `M` is a type with an additive action on `X`, `M` and `X` are topological spaces, and the additive action is continuous, then the function `m ↦ m +ᵥ x` is continuous for all `x : X`.
|
ContinuousOn.smul
theorem ContinuousOn.smul :
∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [inst_4 : ContinuousSMul M X] {f : Y → M} {g : Y → X}
{s : Set Y}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => f x • g x) s
The theorem `ContinuousOn.smul` states that for all types `M`, `X`, and `Y` (given that `M` and `X` are topological spaces and `M` is equipped with an operation of scalar multiplication on `X` which is continuous), and for functions `f : Y → M` and `g : Y → X` as well as a set `s` of type `Y`, if both `f` and `g` are continuous on the set `s`, then the function that maps each element `x` in `s` to the product of `f x` and `g x` (in the sense of scalar multiplication) is also continuous on `s`. This theorem is important in the theory of topological vector spaces, where continuity of operations is a key requirement.
More concisely: If `M` is a topological space equipped with a continuous scalar multiplication, and `f : Y → M` and `g : Y → X` are continuous functions, then the function `x ↦ f x * g x` is continuous on the domain of `f` and `g`.
|
Continuous.vadd
theorem Continuous.vadd :
∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [inst_4 : ContinuousVAdd M X] {f : Y → M} {g : Y → X},
Continuous f → Continuous g → Continuous fun x => f x +ᵥ g x
This theorem states that for any types `M`, `X`, and `Y`, given topological spaces on `M`, `X`, and `Y`, and given that `M` and `X` form a vector space under vector addition, if `f` and `g` are continuous functions from `Y` to `M` and `Y` to `X` respectively, then the function that takes `x` in `Y` and maps it to the vector sum of `f(x)` and `g(x)` is also continuous. This is essentially a formalization of the basic calculus principle that the sum of two continuous functions is also continuous.
More concisely: Given topological spaces on types `M`, `X`, and `Y`, if `M` and `X` form a vector space under vector addition, and `f : Y → M` and `g : Y → X` are continuous functions, then the function `h : Y → M × X` defined by `h x = (f x, g x)` is continuous. (This implies that the vector sum `f x + g x` of `f(x)` and `g(x)` is a continuous function from `Y` to `M`.)
|
ContinuousAt.smul
theorem ContinuousAt.smul :
∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [inst_4 : ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y},
ContinuousAt f b → ContinuousAt g b → ContinuousAt (fun x => f x • g x) b
The theorem states that for any types `M`, `X`, and `Y` equipped with topological space structures, and assuming `M` and `X` also have a scalar multiplication structure, and this scalar multiplication is continuous, then if a function `f` from `Y` to `M` is continuous at a point `b`, and another function `g` from `Y` to `X` is also continuous at the same point, the function that maps `x` in `Y` to the scalar product of `f(x)` and `g(x)` is also continuous at the point `b`.
More concisely: Given types `M` and `X` with topological spaces and scalar multiplication structures, and `Y` with scalar multiplication continuous in `M` and `X`, if `f : Y → M` and `g : Y → X` are continuous at a point `b` in `Y`, then the function `x ↦ f x ⋅ g x` from `Y` to `M` is continuous at `b`. (Here, "⋅" denotes scalar product.)
|
Filter.Tendsto.vadd
theorem Filter.Tendsto.vadd :
∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : VAdd M X] [inst_3 : ContinuousVAdd M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X},
Filter.Tendsto f l (nhds c) →
Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x +ᵥ g x) l (nhds (c +ᵥ a))
This theorem, named `Filter.Tendsto.vadd`, states that for any types `M`, `X` and `α`, with `M` and `X` equipped with a topology and a vector addition operation, and `α` serving as the domain of two functions `f` and `g` with values in `M` and `X` respectively. If `f` tends to a point `c` in `M` and `g` tends to a point `a` in `X` with respect to a filter `l`, and if the vector addition operation is continuous, then the function that at any point `x` gives `f x +ᵥ g x` tends to `c +ᵥ a` with respect to the same filter `l`. In terms of limits, this means that the limit of the vector sum of two functions is the vector sum of their limits, under the given conditions.
More concisely: If functions `f : X → M` and `g : X → X` are each pointwise convergence to their respective limits `c : M` and `a : X` with respect to filter `l`, and vector addition in `M` is continuous, then `f +ᵥ g` pointwise converges to `c +ᵥ a` with respect to `l`.
|
Continuous.smul
theorem Continuous.smul :
∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [inst_4 : ContinuousSMul M X] {f : Y → M} {g : Y → X},
Continuous f → Continuous g → Continuous fun x => f x • g x
This theorem states that for any types `M`, `X`, and `Y`, if `M` and `X` are equipped with a topological space structure and a scalar multiplication operation that is continuous, and if `f` is a continuous function from `Y` to `M` and `g` is a continuous function from `Y` to `X`, then the function which takes an input `x` from `Y` and maps it to the scalar product of `f(x)` and `g(x)` is also continuous.
More concisely: Given continuous scalar multiplication operations on types `M` and `X`, and continuous functions `f: Y → M` and `g: Y → X`, the function `x ↦ (f x) ⊤ (g x)` from `Y` to `M` is continuous, where `⊤` denotes the scalar product.
|
MulAction.continuousSMul_compHom
theorem MulAction.continuousSMul_compHom :
∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Monoid M]
[inst_3 : MulAction M X] [inst_4 : ContinuousSMul M X] {N : Type u_5} [inst_5 : TopologicalSpace N]
[inst_6 : Monoid N] {f : N →* M}, Continuous ⇑f → ContinuousSMul N X
This theorem states that if a multiplication action on a topological space is continuous, then composing this action with a continuous homomorphism from another monoid results in another continuous multiplication action. Specifically, given a monoid `M` and a topological space `X` with a continuous multiplication action, and another monoid `N` with a homomorphism `f` to `M` that is continuous, the multiplication action of `N` on `X` via `f` is also continuous.
More concisely: If `M` is a monoid with a continuous multiplication action on a topological space `X`, and `f` is a continuous homomorphism from another monoid `N` to `M`, then the multiplication action of `N` on `X` via `f` is continuous.
|
Inducing.continuousSMul
theorem Inducing.continuousSMul :
∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [inst_4 : ContinuousSMul M X] {g : Y → X} {N : Type u_5}
[inst_5 : SMul N Y] [inst_6 : TopologicalSpace N] {f : N → M},
Inducing g → Continuous f → (∀ {c : N} {x : Y}, g (c • x) = f c • g x) → ContinuousSMul N Y
This theorem, `Inducing.continuousSMul`, states that if we have two types `N` and `M` acting on types `X` and `Y` respectively, with both actions being continuous, and if there is a homomorphism `g : Y → X` such that there exists a continuous function `f : N → M` satisfying `g (c • x) = f c • g x` for any `c : N` and `x : Y`, then we can conclude that the action of `N` on `Y` is also continuous. This theorem is particularly useful in scenarios such as semilinear maps where `f` might equal `Units.val`.
More concisely: If `N` and `M` are continuous actions on types `Y` and `X` respectively, and there exists a homomorphism `g : Y → X` and a continuous function `f : N → M` such that `g (c • y) = f c • g y` for all `c : N` and `y : Y`, then the action of `N` on `Y` is continuous.
|
Inducing.continuousVAdd
theorem Inducing.continuousVAdd :
∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [inst_4 : ContinuousVAdd M X] {g : Y → X} {N : Type u_5}
[inst_5 : VAdd N Y] [inst_6 : TopologicalSpace N] {f : N → M},
Inducing g → Continuous f → (∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x) → ContinuousVAdd N Y
This theorem, `Inducing.continuousVAdd`, states that if `N` additively acts on `X` and `M` continuously additively acts on `Y`, and there is an additive action homomorphism `g : Y → X` such that there exists a continuous function `f : N → M` satisfying the equation `g (c +ᵥ x) = f c +ᵥ g x` for all `c : N` and `x : Y`, then the additive action of `N` on `X` is also continuous. The theorem extends to scenarios where `f = id`, so `g` is an action homomorphism in the sense of `AddActionHom`, as well as to cases where `f = AddUnits.val`.
More concisely: If `N` additively acts on `X`, `M` continuously additively acts on `Y`, there is an additive action homomorphism `g : Y → X`, and there exists a continuous function `f : N → M` such that `g (c + y) = f c + g y` for all `c : N` and `y : Y`, then the additive action of `N` on `X` is continuous.
|
AddTorsor.connectedSpace
theorem AddTorsor.connectedSpace :
∀ (G : Type u_1) (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P] [inst_2 : TopologicalSpace G]
[inst_3 : PreconnectedSpace G] [inst_4 : TopologicalSpace P] [inst : ContinuousVAdd G P], ConnectedSpace P
This theorem states that if we have a type `G` which is an additive group with a topological space structure and is preconnected, and another type `P` which is an `AddTorsor` over `G` with a topological space structure, then under the condition that the addition operation from `G` to `P` is continuous, `P` is also a connected space. This theorem is not set as an instance as it could lead to an infinite loop when `G` is a torsor over itself.
More concisely: If `G` is a preconnected, additive group with a topology and `P` is a continuous `AddTorsor` over `G` with a topology, then `P` is a connected space.
|