WeakDual.eval_continuous
theorem WeakDual.eval_continuous :
∀ {𝕜 : Type u_2} {E : Type u_5} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
[inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
(y : E), Continuous fun x => x y
This theorem states that for any given type 𝕜 which forms a commutative semiring,𝕜 as a topological space, 𝕜 under continuous addition, 𝕜 under continuous constant scalar multiplication, E as an additive commutative monoid, E as a 𝕜-module, and E as a topological space, the evaluation function (which takes a function 'x' and applies it to an element 'y' of E) is continuous. In other words, for any fixed element 'y' in E, the operation of applying a function to 'y' is a continuous operation.
More concisely: Given a commutative semiring 𝕜, for any continuous addition, continuous scalar multiplication on the 𝕜-module E over 𝕜 as a topological space, the evaluation function from functions to E applying an element is continuous.
|
WeakBilin.embedding
theorem WeakBilin.embedding :
∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
[inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
{B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜}, Function.Injective ⇑B → Embedding fun x y => (B x) y
This theorem states that for any types `𝕜`, `E`, and `F`, if `𝕜` is a topological space, `𝕜` is a commutative semiring, `E` is an additive commutative monoid and a module over `𝕜`, and `F` is an additive commutative monoid and also a module over `𝕜`, then for any linear map `B` from `E` to `F` that maps to `𝕜`, if `B` is an injective function, then the coercion of `B` into a function from `E` to a function from `F` to `𝕜` is an embedding. In other words, if no two distinct elements of `E` map to the same element of `F` under `B`, then we can embed `E` into the space of functions from `F` to `𝕜` using `B`.
More concisely: If `𝕜` is a topological space, commutative semiring, `E` and `F` are additive commutative `𝕜`-modules, `B: E → F` is an injective linear map, then `B` extends to an embedding `B': E �� spett F ↯ 𝕜`.
|
WeakBilin.coeFn_continuous
theorem WeakBilin.coeFn_continuous :
∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
[inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), Continuous fun x y => (B x) y
This theorem states that for any given types 𝕜, E, and F, where 𝕜 is a topological space with a commutative semiring structure, E and F are additively commutative monoids and 𝕜-modules, the function B, which maps an element of E to a linear map from F to 𝕜, is continuous. This means that if we fix an element x in E, and vary y in F, the resulting function is continuous in the topological space structure of 𝕜. Similarly, if we vary x in E, keeping y in F fixed, the function remains continuous.
More concisely: Given a topological space 𝕜 with a commutative semiring structure, and additively commutative monoids and 𝕜-modules E and F, the function B mapping elements of E to linear maps from F to 𝕜 is continuous.
|
WeakBilin.eval_continuous
theorem WeakBilin.eval_continuous :
∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
[inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (y : F), Continuous fun x => (B x) y
This theorem states that, for any type `𝕜` equipped with a topological space structure and a commutative semiring structure, types `E` and `F` equipped with an additive commutative monoid structure and a module structure over `𝕜`, and a bilinear form `B` from `E` to `F` (denoted `E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`), the function `x => (B x) y` is continuous for any `y` in `F`. In mathematical terms, this theorem shows the continuity of the evaluation of a weakly bilinear form.
More concisely: Given a topological space `𝕜` with a commutative semiring structure, types `E` and `F` with additive commutative monoid and `𝕜`-module structures, and a weakly bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, the evaluation map `x ↦ B x y` is continuous for all `y` in `F`.
|