Submodule.le_topologicalClosure
theorem Submodule.le_topologicalClosure :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M),
s ≤ s.topologicalClosure
This theorem states that for any semiring `R`, type `M` with a topological space and additive commutative monoid structures, and `M` being a module over `R` where scalar multiplication is continuous, also addition is continuous, any submodule `s` of `M` is a subset of its topological closure. In other words, it implies that every element of a given submodule is also an element of its topological closure in the context of topological modules.
More concisely: In a topological module over a semiring, every submodule is contained in its topological closure where scalar multiplication and addition are continuous.
|
ContinuousLinearMap.addCommGroup.proof_1
theorem ContinuousLinearMap.addCommGroup.proof_1 :
∀ {M₂ : Type u_1} [inst : TopologicalSpace M₂] [inst_1 : AddCommGroup M₂] [inst_2 : TopologicalAddGroup M₂],
ContinuousAdd M₂
This theorem states that for any type `M₂`, given that `M₂` has a topological space structure, an additive commutative group structure, and a topological additive group structure, it follows that `M₂` has a continuous addition structure. This essentially means that the operation of addition is continuous in the topological sense, i.e., the pre-image of any open set under the addition function is also open.
More concisely: Given a type `M₂` equipped with a topological space, an additive commutative group, and a topological additive group structure, the addition operation on `M₂` is continuous.
|
Module.punctured_nhds_neBot
theorem Module.punctured_nhds_neBot :
∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
[inst_3 : AddCommGroup M] [inst_4 : ContinuousAdd M] [inst_5 : Module R M] [inst_6 : ContinuousSMul R M]
[inst_7 : Nontrivial M] [inst_8 : (nhdsWithin 0 {0}ᶜ).NeBot] [inst : NoZeroSMulDivisors R M] (x : M),
(nhdsWithin x {x}ᶜ).NeBot
The theorem `Module.punctured_nhds_neBot` states the following: Given a topological ring `R` in which zero is not an isolated point (for example, a nontrivially normed field like the reals), and given a nontrivial module `M` over `R` with the property that, if the scalar product of `c` and `x` equals zero, then either `c` equals zero or `x` equals zero, then `M` has no isolated points. This is formulated using the concept of "neighborhood within a set" (`nhdsWithin`). Specifically, the theorem asserts that the set of points in `M` that are not isolated (i.e., for which the "neighborhood within" the set of all points excluding the point itself is nonempty) is nonempty.
More concisely: If `R` is a topological ring with non-isolated zero and `M` is a nontrivial `R`-module satisfying `cx = 0` implies `c = 0` or `x = 0`, then `M` has no isolated points.
|
ContinuousLinearMap.ext_ring
theorem ContinuousLinearMap.ext_ring :
∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
[inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁}, f 1 = g 1 → f = g
This theorem asserts that for any two continuous linear maps `f` and `g` from a semiring `R₁` to a topological module `M₁` over `R₁`, if `f` and `g` map the multiplicative identity (1) of `R₁` to the same value in `M₁`, then `f` and `g` are equal. This means that for these structures, a continuous linear map is uniquely determined by its value at 1.
More concisely: Given two continuous linear maps `f` and `g` from a semiring `R₁` to a topological module `M₁` over `R₁`, if `f` and `g` map the multiplicative identity `1` of `R₁` to the same element in `M₁`, then `f` equals `g`.
|
ContinuousLinearEquiv.ext₁
theorem ContinuousLinearEquiv.ext₁ :
∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
[inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] {f g : R₁ ≃L[R₁] M₁}, f 1 = g 1 → f = g
The theorem, `ContinuousLinearEquiv.ext₁`, states that for any given semiring `R₁`, any topological space and additively commutative monoid `M₁`, any `M₁` module over `R₁`, and any two continuous linear equivalences `f` and `g` from `R₁` to `M₁` (denoted `R₁ ≃L[R₁] M₁` in Lean), if `f` and `g` map the element `1` from `R₁` to the same element in `M₁` (expressed as `f 1 = g 1`), then `f` and `g` are the same continuous linear equivalence (`f = g`). In other words, two continuous linear equivalences between these structures are determined by their values at `1`.
More concisely: Given a semiring `R₁`, a topological space and additively commutative monoid `M₁`, an `R₁`-module `M₁`, and continuous linear equivalences `f` and `g` from `R₁` to `M₁` with `f 1 = g 1`, then `f = g`.
|
ContinuousLinearMap.continuous
theorem ContinuousLinearMap.continuous :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂), Continuous ⇑f
This theorem states that for any continuous linear map `f` from a topological module `M₁` over a semiring `R₁` to a topological module `M₂` over a semiring `R₂`, the function `f` is continuous. Here, `σ₁₂` is a ring homomorphism from `R₁` to `R₂`. Note that `M₁` and `M₂` are not only modules but also topological spaces and commutative monoids, and the continuity of `f` is with respect to the topologies on `M₁` and `M₂`.
More concisely: Given a continuous linear map `f` from a topological module `M₁` over semiring `R₁` to a topological module `M₂` over semiring `R₂` and a ring homomorphism `σ₁₂` from `R₁` to `R₂`, `f` is a continuous function.
|
ContinuousLinearEquiv.ext
theorem ContinuousLinearEquiv.ext :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] {f g : M₁ ≃SL[σ₁₂] M₂}, ⇑f = ⇑g → f = g
This theorem states that for any two continuous linear equivalences `f` and `g` between two topological modules `M₁` and `M₂` over semirings `R₁` and `R₂` respectively, with ring homomorphisms `σ₁₂` and `σ₂₁` that form an inverse pair, if the function corresponding to `f` is equal to the function corresponding to `g`, then `f` itself is equal to `g`. Essentially, this emphasizes that a continuous linear equivalence is determined completely by its corresponding function.
More concisely: If `f` and `g` are continuous linear equivalences between topological modules over semirings with invertible ring homomorphisms forming an inverse pair, and their corresponding functions are equal, then `f` is equal to `g`.
|
Submodule.isClosed_or_dense_of_isCoatom
theorem Submodule.isClosed_or_dense_of_isCoatom :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M),
IsCoatom s → IsClosed ↑s ∨ Dense ↑s
The theorem `Submodule.isClosed_or_dense_of_isCoatom` states that for any given maximal proper subspace of a topological module, which is a `Submodule` satisfying the `IsCoatom` condition (i.e., there is no other element between it and the top element, and it is not the top element itself), the subspace is either a closed set or a dense set in the topological space. In other words, every point of this subspace either belongs to its closure (it's a dense set) or the set contains all its limit points (it's a closed set). This is applicable within the context of a topological module over a semiring where scalar multiplication and addition are continuous operations.
More concisely: In a topological module over a semiring, every maximal proper subspace satisfying the IsCoatom condition is either closed or dense.
|
ContinuousLinearMap.isOpenMap_of_ne_zero
theorem ContinuousLinearMap.isOpenMap_of_ne_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : TopologicalSpace R] [inst_1 : DivisionRing R] [inst_2 : ContinuousSub R]
[inst_3 : AddCommGroup M] [inst_4 : TopologicalSpace M] [inst_5 : ContinuousAdd M] [inst_6 : Module R M]
[inst_7 : ContinuousSMul R M] (f : M →L[R] R), f ≠ 0 → IsOpenMap ⇑f
The theorem `ContinuousLinearMap.isOpenMap_of_ne_zero` states that for any non-zero continuous linear functional `f` from a module `M` over a division ring `R` (where both `M` and `R` have topological structures compatible with their algebraic structures), the function `f` is an open map. In other words, the image of any open set under `f` is also an open set. Here, an open map is defined with respect to the given topological spaces on `M` and `R`.
More concisely: A non-zero continuous linear functional from a topological module over a division ring to itself is an open map.
|
ContinuousLinearMap.smulRight_one_one
theorem ContinuousLinearMap.smulRight_one_one :
∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₂ : Type u_6} [inst_1 : TopologicalSpace M₂] [inst_2 : AddCommMonoid M₂]
[inst_3 : Module R₁ M₂] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₂] (c : R₁ →L[R₁] M₂),
ContinuousLinearMap.smulRight 1 (c 1) = c
The theorem `ContinuousLinearMap.smulRight_one_one` states that for any continuous linear map `c`, in the context of a semiring `R₁`, a topological space `M₂` that is also an additive commutative monoid and a module over `R₁`, with continuous scalar multiplication from `R₁` to `M₂`, and a topology on `R₁`, `c` applied to 1 is equivalent to scalar multiplication by 1 (using `smulRight`) on the result of `c` applied to 1. This essentially says that scalar multiplication by 1 does not change the output of the continuous linear map when applied to 1.
More concisely: For any continuous linear map `c` from a semiring `R₁` to a topological additive commutative monoid and module `M₂` over `R₁`, with continuous scalar multiplication, `c(1) = smulRight 1 (c 1)` in `M₂`.
|
ContinuousLinearMap.coe_mk
theorem ContinuousLinearMap.coe_mk :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂)
(h : Continuous f.toFun), ↑{ toLinearMap := f, cont := h } = f
This theorem, `ContinuousLinearMap.coe_mk`, states that for any continuous linear mapping `f` from a topological module `M₁` over a semiring `R₁` to a topological module `M₂` over a semiring `R₂` with a given semiring homomorphism `σ₁₂`, when `f` is incorporated into a continuous linear map structure `{ toLinearMap := f, cont := h }` (where `h` is the proof of continuity of `f`), the coercion of this structure back to a function gives the original function `f`. This essentially means that the process of packaging a continuous linear map into a structure and coercing it back doesn't alter the underlying function.
More concisely: The coercion of a continuous linear map from one topological module to another, equipped with its continuity proof, back to a function preserves the original mapping.
|
ContinuousLinearMap.map_sub
theorem ContinuousLinearMap.map_sub :
∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
[inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
[inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x y : M),
f (x - y) = f x - f y
This theorem states that for any continuous linear map `f` from a module `M` over a ring `R` to a module `M₂` over a ring `R₂`, the mapping preserves subtraction. More specifically, for all elements `x` and `y` in `M`, applying the map `f` to the difference of `x` and `y` (`f (x - y)`) yields the same result as subtracting the mapping of `y` from the mapping of `x` (`f x - f y`). This property holds for any topological spaces `M` and `M₂` that also have an additive commutative group structure, and any ring homomorphism `σ₁₂` from `R` to `R₂`.
More concisely: For any continuous linear map $f$ from a module $M$ over a ring $R$ to a module $M\_2$ over a ring $R\_2$ and any ring homomorphism $\sigma \_{12}: R \rightarrow R\_2$, the equation $f(x - y) = f(x) - f(y)$ holds for all $x, y \in M$.
|
ContinuousSemilinearEquivClass.map_continuous
theorem ContinuousSemilinearEquivClass.map_continuous :
∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst_1 : Semiring S]
{σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
{M : outParam (Type u_4)} [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] {M₂ : outParam (Type u_5)}
[inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M] [inst_9 : Module S M₂]
[inst_10 : EquivLike F M M₂] [self : ContinuousSemilinearEquivClass F σ M M₂] (f : F), Continuous ⇑f
The theorem `ContinuousSemilinearEquivClass.map_continuous` asserts that for any type `F`, given a semilinear equivalence between two modules `M` and `M₂` over two semirings `R` and `S` (with ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` forming an inverse pair), the map `f : F` representing this equivalence is continuous. Here, a map `f` is semilinear if it preserves addition (i.e., `f (x + y) = f x + f y`) and scalar multiplication is twisted by `σ` (i.e., `f (c • x) = (σ c) • f x`). This theorem is applicable when `M` and `M₂` are topological modules and `F` is an equivalence class of continuous semilinear maps from `M` to `M₂`.
More concisely: Given a semilinear equivalence between topological modules over commutative semirings with invertible ring homomorphisms, the representing map is a continuous linear transformation.
|
ContinuousLinearMap.inverse_equiv
theorem ContinuousLinearMap.inverse_equiv :
∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
[inst_2 : Semiring R] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : AddCommMonoid M]
[inst_6 : Module R M] (e : M ≃L[R] M₂), (↑e).inverse = ↑e.symm
The theorem `ContinuousLinearMap.inverse_equiv` states that for any continuous linear equivalence `e` between two topological modules `M` and `M₂` over a semiring `R`, the inverse of `e` is equal to the symmetric of `e`. In other words, if `e` is a continuous linear map that is invertible, then the inverse of `e` is exactly the same as the map that reverses the direction of `e`.
More concisely: For any continuous linear equivalence between topological modules over a semiring, its inverse is equal to its symmetric.
|
ContinuousLinearEquiv.continuous
theorem ContinuousLinearEquiv.continuous :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), Continuous ⇑e
This theorem states that for any continuous linear equivalence 'e' from a topological module 'M₁' over a semi-ring 'R₁' to a topological module 'M₂' over a semi-ring 'R₂', with the rings equipped with a pair of inverse ring homomorphisms, the application function of 'e' is continuous. Hence, you can map elements continuously from one module to another using this equivalence.
More concisely: Given continuous linear equivalences between topological modules over semi-rings with inverse ring homomorphisms, the application function is continuous.
|
ContinuousLinearEquiv.uniformEmbedding
theorem ContinuousLinearEquiv.uniformEmbedding :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_9} {E₂ : Type u_10}
[inst_4 : UniformSpace E₁] [inst_5 : UniformSpace E₂] [inst_6 : AddCommGroup E₁] [inst_7 : AddCommGroup E₂]
[inst_8 : Module R₁ E₁] [inst_9 : Module R₂ E₂] [inst_10 : UniformAddGroup E₁] [inst_11 : UniformAddGroup E₂]
(e : E₁ ≃SL[σ₁₂] E₂), UniformEmbedding ⇑e
This Lean theorem, `ContinuousLinearEquiv.uniformEmbedding`, states that for any two types `R₁` and `R₂` equipped with semiring structures, and any two ring homomorphisms `σ₁₂` from `R₁` to `R₂` and `σ₂₁` from `R₂` to `R₁` that form an inverse pair, and any two types `E₁` and `E₂` that have uniform spaces, additive commutative group structures, and are modules over `R₁` and `R₂` respectively, and are also equipped with uniform additive group structures, any continuous linear equivalence `e` from `E₁` to `E₂` (with respect to the ring homomorphism `σ₁₂`) is a uniform embedding. In simpler terms, a continuous linear equivalence between two appropriate mathematical structures is always a uniform embedding.
More concisely: A continuous linear equivalence between two uniformly equipped, ring-module structures over commutative semirings, with inversely compatible ring homomorphisms, is a uniform embedding.
|
ContinuousLinearMap.to_ring_inverse
theorem ContinuousLinearMap.to_ring_inverse :
∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
[inst_2 : Ring R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup M₂]
[inst_6 : Module R M₂] (e : M ≃L[R] M₂) (f : M →L[R] M₂),
f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm
This theorem states that for any topological spaces `M` and `M₂` and a ring `R`, given a continuous linear equivalence `e` between `M` and `M₂` and a continuous linear map `f` from `M` to `M₂`, the inverse of `f` can be expressed in terms of the `Ring.inverse` function. Specifically, it's equal to the composition of the inverse of the `Ring.inverse` of the composition of `f` and the inverse of `e`, with the inverse of `e`. This composition uses ring operations in the ring of self-maps (functions from a space to itself) of `M`.
More concisely: For any continuous linear equivalence `e` between topological spaces `M` and `M₂` and a continuous linear map `f` from `M` to `M₂`, the inverse of `f` is equal to the composition of the inverse of `e`, the inverse of the composition of `f` and `e`, and the inverse of `e` in the ring of self-maps of `M`.
|
ContinuousLinearMap.smulRight_one_pow
theorem ContinuousLinearMap.smulRight_one_pow :
∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalRing R] (c : R) (n : ℕ),
ContinuousLinearMap.smulRight 1 c ^ n = ContinuousLinearMap.smulRight 1 (c ^ n)
This theorem states that for any ring `R` that also has the structure of a topological space and a topological ring, and for any element `c` of `R` and natural number `n`, raising the continuous linear map that scales by `c` to the power of `n` is equal to the continuous linear map that scales by `c` raised to the power of `n`. In mathematical terms, this means that (1 * c)^n = 1 * (c^n) when working with continuous linear maps in a topological ring.
More concisely: For any continuous linear map scaling element `c` in a topological ring `R`, (scaling map)^n = scaling map^n.
|
ContinuousLinearMap.eqOn_closure_span
theorem ContinuousLinearMap.eqOn_closure_span :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : T2Space M₂] {s : Set M₁}
{f g : M₁ →SL[σ₁₂] M₂}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn (⇑f) (⇑g) (closure ↑(Submodule.span R₁ s))
This theorem states that if two continuous linear maps, represented as `f` and `g`, are equal on a set `s` of elements of some type `M₁`, then they are also equal on the closure of the `Submodule.span` of this set `s`. Here, the `Submodule.span` of `s` is the smallest submodule that contains `s`, and the `closure` is the smallest closed set containing this span. The parameters `R₁` and `R₂` are semirings, `σ₁₂` is a ring homomorphism from `R₁` to `R₂`, and `M₁` and `M₂` are modules over `R₁` and `R₂` respectively. `M₁` and `M₂` are also equipped with a topological space structure and `M₂` is a `T2Space`, also known as a Hausdorff space. The maps `f` and `g` are continuous linear maps from `M₁` to `M₂`. The theorem is proven using the definition of `Set.EqOn`, which states that two functions are equal on a set if they map any element of the set to the same value.
More concisely: If two continuous linear maps between topological modules over compatible semirings are equal on a set and its span, then they are equal on the closure of that set's span.
|
ContinuousLinearMap.ext
theorem ContinuousLinearMap.ext :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂},
(∀ (x : M₁), f x = g x) → f = g
This theorem states that for any two continuous linear maps `f` and `g` from a module `M₁` over a semiring `R₁` to a module `M₂` over a semiring `R₂`, under a specific ring homomorphism `σ₁₂` from `R₁` to `R₂`, if `f` and `g` are equal at all points `x` in `M₁`, then `f` and `g` themselves are equal. This theorem basically guarantees the extensionality of continuous linear maps, meaning that two continuous linear maps are equal if they are equal on every element of their domain.
More concisely: Given continuous linear maps `f` and `g` from module `M₁` over semiring `R₁` to module `M₂` over semiring `R₂`, and a ring homomorphism `σ₁₂` from `R₁` to `R₂`, if `f(x) = g(x)` for all `x` in `M₁`, then `f = g`.
|
ContinuousLinearMap.coe_injective
theorem ContinuousLinearMap.coe_injective :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂],
Function.Injective ContinuousLinearMap.toLinearMap
The theorem `ContinuousLinearMap.coe_injective` states that for any two semirings `R₁` and `R₂`, a ring homomorphism `σ₁₂ : R₁ →+* R₂`, two types `M₁` and `M₂` with topological spaces and additive commutative monoid structures, and module structures over `R₁` and `R₂` respectively, the function `ContinuousLinearMap.toLinearMap`, which converts a continuous linear map to a linear map, is injective. In other words, if two continuous linear maps are mapped to the same linear map by `ContinuousLinearMap.toLinearMap`, those two continuous linear maps must have been the same to start with.
More concisely: Given semirings `R₁` and `R₂`, ring homomorphisms `σ₁₂ : R₁ →+* R₂`, and topological vector spaces `M₁` and `M₂` with additive commutative monoid structures and module structures over `R₁` and `R₂` respectively, the function `ContinuousLinearMap.toLinearMap` mapping continuous linear maps from `M₁` to `M₂` to their underlying linear maps is injective.
|
TopologicalSpace.IsSeparable.span
theorem TopologicalSpace.IsSeparable.span :
∀ {R : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
[inst_3 : TopologicalSpace M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace.SeparableSpace R]
[inst_6 : ContinuousAdd M] [inst_7 : ContinuousSMul R M] {s : Set M},
TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable ↑(Submodule.span R s)
This theorem states that given a separable subset `s` of a topological space `M` with respect to a separable scalar ring `R`, the span of `s` (which is the smallest submodule of `M` containing `s`) is also separable. Here, a set is considered separable in a topological space if it can be contained within the closure of a countable set. The theorem also requires the conditions that addition in `M` and scalar multiplication by `R` in `M` are continuous operations. In summary, the separability property is preserved under the operation of span in this context.
More concisely: If `s` is a separable subset of a topological space `M` with respect to a separable scalar ring `R`, where addition and scalar multiplication in `M` are continuous, then the span of `s` is also a separable subset of `M`.
|
DenseRange.topologicalClosure_map_submodule
theorem DenseRange.topologicalClosure_map_submodule :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : RingHomSurjective σ₁₂]
[inst_9 : TopologicalSpace R₁] [inst_10 : TopologicalSpace R₂] [inst_11 : ContinuousSMul R₁ M₁]
[inst_12 : ContinuousAdd M₁] [inst_13 : ContinuousSMul R₂ M₂] [inst_14 : ContinuousAdd M₂] {f : M₁ →SL[σ₁₂] M₂},
DenseRange ⇑f →
∀ {s : Submodule R₁ M₁}, s.topologicalClosure = ⊤ → (Submodule.map (↑f) s).topologicalClosure = ⊤
The theorem `DenseRange.topologicalClosure_map_submodule` states that for any semirings `R₁` and `R₂`, a continuous linear map `f` from `M₁` to `M₂` (where `M₁` and `M₂` are topological modules over `R₁` and `R₂` respectively), a surjective ring homomorphism `σ₁₂` from `R₁` to `R₂`, and a submodule `s` of `M₁` such that its topological closure is the whole space `M₁`, if the range of `f` is dense in `M₂`, then the topological closure of the image of `s` under `f` is also the whole space `M₂`. In other words, the image of a dense set under a continuous linear map with dense range is also dense.
More concisely: If `f` is a continuous linear map from a topological module `M₁` over semiring `R₁` to a topological module `M₂` over semiring `R₂`, `σ₁₂` is a surjective ring homomorphism from `R₁` to `R₂`, `s` is a submodule of `M₁` with topological closure equal to `M₁`, and the range of `f` is dense in `M₂`, then the topological closure of `f(s)` equals `M₂`.
|
Submodule.dense_iff_topologicalClosure_eq_top
theorem Submodule.dense_iff_topologicalClosure_eq_top :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] {s : Submodule R M},
Dense ↑s ↔ s.topologicalClosure = ⊤
The theorem states that for any given submodule `s` of a module `M` over a semiring `R` with a topological space structure, continuous scalar multiplication, and continuous addition, the submodule `s` is dense if and only if the topological closure of `s` equals the whole space. In other words, a submodule is dense in the space if every point in the space can either be reached from the submodule by a sequence of steps within the submodule, or is in the submodule itself.
More concisely: A submodule of a topological module is dense if and only if its topological closure equals the entire module.
|
ContinuousLinearEquiv.image_symm_eq_preimage
theorem ContinuousLinearEquiv.image_symm_eq_preimage :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂), ⇑e.symm '' s = ⇑e ⁻¹' s
The theorem `ContinuousLinearEquiv.image_symm_eq_preimage` states that for any semirings `R₁` and `R₂` with ring homomorphisms `σ₁₂` from `R₁` to `R₂` and `σ₂₁` from `R₂` to `R₁` that form a ring homomorphism inverse pair, and for any topological spaces `M₁` and `M₂` that are also additively commutative monoids and modules over `R₁` and `R₂` respectively, given a continuous linear equivalence `e` from `M₁` to `M₂` and a set `s` in `M₂`, the image under the inverse of `e` of the set `s` is equal to the preimage of the set `s` under `e`. In simpler terms, applying the inverse of the equivalence `e` to a set `s` gives the same result as finding all points in the domain of `e` that `e` would map into `s`.
More concisely: For any continuous linear equivalence between additively commutative monoids and modules over commutative semirings, the image of a set under the inverse of the equivalence equals the preimage of that set.
|
ContinuousLinearEquiv.symm_apply_apply
theorem ContinuousLinearEquiv.symm_apply_apply :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁), e.symm (e b) = b
This is a theorem about continuous linear equivalences between two topological modules over semirings. Specifically, it states that for any semirings R₁ and R₂ with ring homomorphisms σ₁₂ from R₁ to R₂ and σ₂₁ from R₂ to R₁, and any two topological modules M₁ and M₂ over R₁ and R₂ respectively, if we have a continuous linear equivalence 'e' from M₁ to M₂, applying 'e' to an element 'b' in M₁ and then applying the inverse of 'e' gives us back the original element 'b'. This asserts that the continuous linear equivalence and its inverse are indeed inverses of each other in the category of topological modules.
More concisely: Given semirings R₁ and R₂ with ring homomorphisms σ₁₂ and σ₂₁, and topological modules M₁ over R₁ and M₂ over R₂ with a continuous linear equivalence e : M₁ ≈ M₂, e ∘ e⁻¹ = id on M₁ and e⁻¹ ∘ e = id on M₂.
|
ContinuousLinearMap.map_neg
theorem ContinuousLinearMap.map_neg :
∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
[inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
[inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M), f (-x) = -f x
The theorem `ContinuousLinearMap.map_neg` states that for any ring `R`, another ring `R₂`, a topological space `M` over `R` that is also an additive commutative group, another topological space `M₂` over `R₂` that is also an additive commutative group, and a continuous linear map `f` from `M` to `M₂`, the image of the negative of a point `x` in `M` under `f` is equal to the negative of the image of `x` under `f`. This effectively shows that continuous linear maps preserve the negation operation.
More concisely: For any continuous linear map `f` between additive commutative groups and topological spaces `M` over ring `R` and `M₂` over ring `R₂`, respectively, we have `f(-x) = -(f(x))` for all `x` in `M`.
|
ContinuousLinearMap.ext_on
theorem ContinuousLinearMap.ext_on :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : T2Space M₂] {s : Set M₁},
Dense ↑(Submodule.span R₁ s) → ∀ {f g : M₁ →SL[σ₁₂] M₂}, Set.EqOn (⇑f) (⇑g) s → f = g
This theorem states that for any two semirings `R₁` and `R₂`, and any type `M₁` with a topological structure, additive commutative monoid structure, and a module structure over `R₁`, and any type `M₂` with a topological structure, additive commutative monoid structure, a module structure over `R₂`, and a `T2Space` (also known as a Hausdorff space) structure, if the submodule generated by a set `s` of elements of `M₁` is dense in the module `M₁`, then any two continuous linear maps from `M₁` to `M₂` that are equal on `s` are equal everywhere. In other words, if two continuous linear maps agree on a set whose span is dense, they must be the same map.
More concisely: Given semirings `R₁` and `R₂`, types `M₁` with dense submodule `s` and topological, additive commutative monoid, and `R₁`-module structures, and type `M₂` with topological structure, additive commutative monoid structure, `R₂`-module structure, and a `T2Space` structure, any two continuous linear maps from `M₁` to `M₂` that agree on `s` are equal.
|
ContinuousLinearEquiv.symm_image_image
theorem ContinuousLinearEquiv.symm_image_image :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁), ⇑e.symm '' (⇑e '' s) = s
The theorem `ContinuousLinearEquiv.symm_image_image` states that for any two types `R₁` and `R₂` equipped with semiring structures, two homomorphisms `σ₁₂` and `σ₂₁` between them forming a ring homomorphism inverse pair, types `M₁` and `M₂` equipped with topological space structures, additive commutative monoid structures, and modules over `R₁` and `R₂` respectively, along with a continuous linear equivalence `e` from `M₁` to `M₂`, and a set `s` of type `M₁`, applying `e` to `s`, and then applying the inverse of `e` to the image, gives back the original set `s`. This theorem essentially captures the idea that a continuous linear equivalence and its inverse act as a bijective map and its inverse in the context of sets.
More concisely: For any continuous linear equivalence between additive commutative monoids equipped with semiring structures and module structures over two rings, with inverse pair, the preimage of an image of a set under this equivalence and its inverse is the original set.
|
ContinuousLinearMap.map_zero
theorem ContinuousLinearMap.map_zero :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂), f 0 = 0
The theorem `ContinuousLinearMap.map_zero` states that for any continuous linear map `f` from a topological module `M₁` over a semiring `R₁` to a topological module `M₂` over another semiring `R₂`, the map of zero from `M₁` (denoted `f 0`) is zero in `M₂`. Here, `σ₁₂` is a ring homomorphism from `R₁` to `R₂`, `inst_2` and `inst_4` state that `M₁` and `M₂` are topological spaces, `inst_3` and `inst_5` state that `M₁` and `M₂` are commutative monoids, and `inst_6` and `inst_7` provide the module structures of `M₁` over `R₁` and `M₂` over `R₂` respectively.
More concisely: For any continuous linear map `f` from a topological module `M₁` over semiring `R₁` to a topological module `M₂` over semiring `R₂` with a ring homomorphism `σ₁₂` from `R₁` to `R₂`, `f 0 = 0` in `M₂`, where `0` denotes the additive identity in `M₁` and `M₂`.
|
Submodule.topologicalClosure_map
theorem Submodule.topologicalClosure_map :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : RingHomSurjective σ₁₂]
[inst_9 : TopologicalSpace R₁] [inst_10 : TopologicalSpace R₂] [inst_11 : ContinuousSMul R₁ M₁]
[inst_12 : ContinuousAdd M₁] [inst_13 : ContinuousSMul R₂ M₂] [inst_14 : ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂)
(s : Submodule R₁ M₁), Submodule.map (↑f) s.topologicalClosure ≤ (Submodule.map (↑f) s).topologicalClosure
The theorem, `Submodule.topologicalClosure_map`, states that for any continuous linear map `f` from a `TopologicalSpace` `M₁` to another `TopologicalSpace` `M₂`, where `M₁` and `M₂` are modules over semirings `R₁` and `R₂` respectively and `σ₁₂` is a ring homomorphism from `R₁` to `R₂`, when this map `f` is applied to the topological closure of a submodule `s` of `M₁`, the resulting set is a subset of the topological closure of the image of `s` under `f`. In other words, the image of the topological closure of a submodule under a continuous linear map is contained within the topological closure of its image.
More concisely: For any continuous linear map between topological modules over compatible semirings and their ring homomorphisms, the image of the topological closure of a submodule is contained in the topological closure of its image.
|
ContinuousLinearEquiv.continuous_invFun
theorem ContinuousLinearEquiv.continuous_invFun :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
[inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
[inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R M] [inst_9 : Module S M₂] (self : M ≃SL[σ] M₂), Continuous self.invFun
This theorem states that for any continuous linear equivalence between two modules `M` and `M₂` over semirings `R` and `S` respectively, where `M` and `M₂` are topological modules over the topological semiring `R` in most applications, the inverse function of this linear equivalence is continuous. The theorem is defined under the conditions that `R` and `S` are semirings, `σ` and `σ'` are ring homomorphisms that form an inverse pair, `M` and `M₂` are topological spaces with additive commutative monoid structures, and `M` and `M₂` are modules over `R` and `S` respectively.
More concisely: If `σ: R -> S` is a ring homomorphism with inverse `σ': S -> R`, `M` is a topological module over the semiring `R`, `M₂` is a topological module over the semiring `S`, and `f: M -> M₂` is a continuous linear equivalence, then `f⁻¹` is a continuous function.
|
ContinuousLinearEquiv.continuous_toFun
theorem ContinuousLinearEquiv.continuous_toFun :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
[inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
[inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R M] [inst_9 : Module S M₂] (self : M ≃SL[σ] M₂), Continuous self.toFun
This theorem states that for any continuous linear equivalence between two modules M and M₂ over semirings R and S respectively, under certain conditions, the function that maps elements of M to M₂ is continuous. The conditions include: R and S being semirings, existence of ring homomorphisms σ from R to S and σ' from S to R that form an inverse pair, M and M₂ being topological spaces and additive commutative monoids, and M and M₂ being modules over R and S respectively.
More concisely: Given continuous linear equivalences between modules M over semiring R and M₂ over semiring S, and semiring homomorphisms σ from R to S and σ' from S to R forming an inverse pair, the function induced by the equivalence is continuous.
|
ContinuousLinearMap.map_add
theorem ContinuousLinearMap.map_add :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (x y : M₁),
f (x + y) = f x + f y
This theorem states that for any two elements `x` and `y` of a module `M₁` over a semiring `R₁`, and a continuous linear map `f` from `M₁` to another module `M₂` over a semiring `R₂` with respect to a ring homomorphism `σ₁₂` from `R₁` to `R₂`, the result of applying `f` to the sum of `x` and `y` (`f (x + y)`) is equal to the sum of the results of applying `f` to `x` and `y` separately (`f x + f y`). In other words, the continuous linear map `f` preserves addition.
More concisely: For any semirings R₁, R₂, modules M₁ over R₁ and M₂ over R₂, and continuous linear map f from M₁ to M₂ over R₂ via a ring homomorphism σ₁₂, we have f (x + y) = f x + f y for all x, y in M₁.
|
ContinuousSemilinearEquivClass.inv_continuous
theorem ContinuousSemilinearEquivClass.inv_continuous :
∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst_1 : Semiring S]
{σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
{M : outParam (Type u_4)} [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] {M₂ : outParam (Type u_5)}
[inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M] [inst_9 : Module S M₂]
[inst_10 : EquivLike F M M₂] [self : ContinuousSemilinearEquivClass F σ M M₂] (f : F),
Continuous (EquivLike.inv f)
The theorem `ContinuousSemilinearEquivClass.inv_continuous` states that for any type `F`, semirings `R` and `S`, ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` that form a pair of inverses, and types `M` and `M₂` with given topological spaces, additive commutative monoids, and modules over `R` and `S` respectively, if `F` represents a class of continuous `σ`-semilinear equivalences from `M` to `M₂` (meaning that it satisfies the properties `f (x + y) = f x + f y` and `f (c • x) = (σ c) • f x`), then the inverse mapping `EquivLike.inv f` for any `f : F` is continuous.
More concisely: Given type `F` of continuous `σ-${semilinear}$` equivalences from additive commutative monoids `M` to `M₂` over rings `R` and `S` with ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` as inverses, any such equivalence `f : F` has a continuous inverse.
|
Submodule.eq_top_of_nonempty_interior'
theorem Submodule.eq_top_of_nonempty_interior' :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
[inst_3 : AddCommGroup M] [inst_4 : ContinuousAdd M] [inst_5 : Module R M] [inst_6 : ContinuousSMul R M]
[inst_7 : (nhdsWithin 0 {x | IsUnit x}).NeBot] (s : Submodule R M), (interior ↑s).Nonempty → s = ⊤
This theorem states that if `M` is a topological module over a ring `R`, and zero is a limit of invertible elements of `R` (for example, if `R` is a nontrivially normed field), then the entire `M` (`⊤`) is the only submodule of `M` that has a nonempty interior. In other words, if a submodule of `M` has a nonempty interior, it must be the entire module `M`. Here, interior refers to the largest open subset of a given set and a set is open if it is a neighborhood of all its points. The interior of a submodule is nonempty if there exists at least one open subset within the submodule.
More concisely: If `M` is a topological module over a ring `R` with zero being a limit of invertible elements, then the only submodule of `M` with a nonempty interior is the entire module `M`.
|
ContinuousLinearEquiv.apply_symm_apply
theorem ContinuousLinearEquiv.apply_symm_apply :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : M₂), e (e.symm c) = c
This theorem states that for any semirings `R₁` and `R₂` with ring homomorphisms `σ₁₂` and `σ₂₁` forming an inverse pair, and any types `M₁` and `M₂` that are topological spaces, additive commutative monoids, and modules over `R₁` and `R₂` respectively, and for any continuous linear equivalence `e` between `M₁` and `M₂`, the application of `e` after the application of the inverse of `e` to any element `c` of `M₂` results in `c`. In other words, applying a continuous linear equivalence and its inverse in succession is the identity operation on `M₂`. The proof for this mathematical statement is not shown here.
More concisely: For any continuous linear equivalence between topological semimodules over commutative semirings with inverse homomorphisms, the composition of the equivalence and its inverse is the identity.
|
ContinuousLinearMap.zero_apply
theorem ContinuousLinearMap.zero_apply :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (x : M₁), 0 x = 0
This theorem states that for any semirings `R₁` and `R₂`, any continuous linear map `σ₁₂` from `R₁` to `R₂`, any topological space and additive commutative monoid `M₁` over `R₁`, and any topological space and additive commutative monoid `M₂` over `R₂`, applying the zero continuous linear map to any element `x` in `M₁` results in the zero element of `M₂`.
More concisely: For any continuous linear maps σ₁₂ between semirings R₁ and R₂, and additive commutative monoids M₁ over R₁ and M₂ over R₂, we have σ₁₂(0ₘ₁) = 0ₘ₂, where 0ₘ₁ denotes the zero element of M₁ and 0ₘ₂ denotes the zero element of M₂.
|
ContinuousLinearMap.uniformContinuous
theorem ContinuousLinearMap.uniformContinuous :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {E₁ : Type u_9}
{E₂ : Type u_10} [inst_2 : UniformSpace E₁] [inst_3 : UniformSpace E₂] [inst_4 : AddCommGroup E₁]
[inst_5 : AddCommGroup E₂] [inst_6 : Module R₁ E₁] [inst_7 : Module R₂ E₂] [inst_8 : UniformAddGroup E₁]
[inst_9 : UniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂), UniformContinuous ⇑f
The theorem `ContinuousLinearMap.uniformContinuous` asserts that for any two types `R₁` and `R₂` equipped with semiring structures, a homomorphism `σ₁₂` from `R₁` to `R₂`, two types `E₁` and `E₂` equipped with uniform space, additive group, and module structures, and given that `E₁` and `E₂` are uniform additive groups, any continuous linear map `f` from `E₁` to `E₂` with respect to the ring homomorphism `σ₁₂` is uniformly continuous. In simpler terms, this theorem states that any continuous linear map between two uniform additive groups is uniformly continuous, meaning that the map's output values remain close together when the input values are close together, regardless of where these input values are located within the input space.
More concisely: Given uniform additive groups `E₁` and `E₂`, a continuous linear map `f` from `E₁` to `E₂` with respect to a ring homomorphism is uniformly continuous.
|
ContinuousLinearMap.inverse_non_equiv
theorem ContinuousLinearMap.inverse_non_equiv :
∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
[inst_2 : Semiring R] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : AddCommMonoid M]
[inst_6 : Module R M] (f : M →L[R] M₂), (¬∃ e', ↑e' = f) → f.inverse = 0
The theorem `ContinuousLinearMap.inverse_non_equiv` states that for any continuous linear map `f` from a module `M` to another module `M₂` over a semiring `R` (where `M` and `M₂` are topological spaces), if `f` is not invertible (that is, there does not exist an inverse map `e'` such that `e'` when coerced is equal to `f`), then the inverse of `f` is equal to the zero map.
More concisely: If a continuous linear map `f` from module `M` to `M₂` over a semiring `R` does not have an inverse, then its inverse is the zero map.
|
IsClosed.submodule_topologicalClosure_eq
theorem IsClosed.submodule_topologicalClosure_eq :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] {s : Submodule R M},
IsClosed ↑s → s.topologicalClosure = s
This theorem states that for a given closed submodule `s` of a module `M` over a semiring `R`, its topological closure is equal to `s` itself. This is under the conditions that `M` has a topological space structure, additive commutative monoid structure, and `R`-module structure, and the scalar multiplication and addition in `M` are continuous. Hence, in this situation, the topological closure operation does not modify a closed submodule.
More concisely: The topological closure of a closed submodule of a topological additive commutative R-module with continuous scalar multiplication and addition is equal to the submodule itself.
|
ContinuousLinearMap.toSpanSingleton_smul
theorem ContinuousLinearMap.toSpanSingleton_smul :
∀ (R : Type u_10) {M₁ : Type u_11} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
[inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace M₁] [inst_5 : ContinuousSMul R M₁] (c : R) (x : M₁),
ContinuousLinearMap.toSpanSingleton R (c • x) = c • ContinuousLinearMap.toSpanSingleton R x
This theorem states that for any commutative semiring `R`, any additive commutative monoid `M₁` that is also a module over `R`, and any elements `c` from `R` and `x` from `M₁`, transforming the scalar multiple `c • x` into a singleton span using the `toSpanSingleton` function from `ContinuousLinearMap` is equal to the scalar multiple `c` times the singleton span of `x`. This holds true under the conditions that `R` and `M₁` are topological spaces and that the scalar multiplication operation in `M₁` is continuous.
More concisely: For any commutative semiring `R`, any additive commutative `R`-module `M₁` that is a topological space, and any continuous scalar multiplication, the map `toSpanSingleton (c • x)` from `ContinuousLinearMap R M₁` equals the scalar multiple `c` times the singleton span of `x` in `M₁`.
|
ContinuousLinearMap.coe_smul
theorem ContinuousLinearMap.coe_smul :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {S₂ : Type u_9} [inst_8 : Monoid S₂]
[inst_9 : DistribMulAction S₂ M₂] [inst_10 : SMulCommClass R₂ S₂ M₂] [inst_11 : ContinuousConstSMul S₂ M₂]
(c : S₂) (f : M₁ →SL[σ₁₂] M₂), ↑(c • f) = c • ↑f
The theorem `ContinuousLinearMap.coe_smul` states that for any semirings `R₁` and `R₂`, a continuous semilinear map `f` from topological space `M₁` to `M₂` (both of which are commutative monoids), and scalar `c` from a monoid `S₂` that acts distributively on `M₂` and commutes with `R₂` under scalar multiplication, the coercion of the product of `c` and `f` (`c • f`) is equal to the scalar multiplication of `c` and the coercion of `f` (`c • ↑f`). This theory assumes `S₂` continuously acts on `M₂` by scalar multiplication.
More concisely: For any commutative monoids M₁ and M₂, semirings R₁ and R₂, a continuous semilinear map f from M₁ to M₂, and a scalar c from a monoid S₂ that distributes over M₂ and commutes with R₂ under scalar multiplication, the coercion of the product of c and f is equal to the scalar multiplication of c by the coercion of f: c • f = c • ↑f.
|
ContinuousLinearMap.cont
theorem ContinuousLinearMap.cont :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_3}
[inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂] (self : M →SL[σ] M₂),
Continuous self.toFun
This theorem declares that for any given semirings `R` and `S`, a ring homomorphism `σ` from `R` to `S`, types `M` and `M₂` representing topological modules over `R` and `S` respectively equipped with topological spaces and additive commutative monoid structures, and a continuous linear map `self` from `M` to `M₂` (indicated by `M →SL[σ] M₂`), the function `self.toFun` underlying the linear map is continuous.
More concisely: Given semirings R and S, a ring homomorphism σ from R to S, and continuous linear maps self : M →SL[σ] M₂ between topological modules M over R and M₂ over S, the underlying function of self is continuous.
|
ContinuousLinearEquiv.surjective
theorem ContinuousLinearEquiv.surjective :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
[inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
[inst_5 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), Function.Surjective ⇑e
The theorem `ContinuousLinearEquiv.surjective` states that for any two types `R₁` and `R₂` with semiring structures, given two ring homomorphisms `σ₁₂ : R₁ →+* R₂` and `σ₂₁ : R₂ →+* R₁` that form a ring homomorphism inverse pair, and any two types `M₁` and `M₂` with topological space and additive commutative monoid structures, and modules over `R₁` and `R₂` respectively, then for every continuous linear equivalence `e : M₁ ≃SL[σ₁₂] M₂`, the function `e` is surjective. In other words, for every element in `M₂`, there exists an element in `M₁` such that applying `e` to this element of `M₁` yields the element in `M₂`.
More concisely: Given continuous linear equivalences between topological additive commutative monoids and modules over commutative semirings with invertible ring homomorphisms, the equivalence is surjective.
|
ContinuousLinearMap.map_smul
theorem ContinuousLinearMap.map_smul :
∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
{M₂ : Type u_6} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
[inst_6 : Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁), f (c • x) = c • f x
This theorem states that for any continuous linear map `f` from a module `M₁` to another module `M₂` over the same semiring `R₁`, and for any element `c` from `R₁` and `x` from `M₁`, the map of the scaled element `c • x` under `f` is equal to the scaled map of `x` under `f`, i.e., `f (c • x) = c • f x`. This is essentially an expression of the homogeneity property of linear maps in the context of topological vector spaces.
More concisely: For any continuous linear map $f$ between modules $M\_1$ and $M\_2$ over the same semiring $R$, and for all $c \in R$ and $x \in M\_1$, we have $f(c \cdot x) = c \cdot f(x)$.
|