WithSeminorms.T1_of_separating
theorem WithSeminorms.T1_of_separating :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ (โ (x : E), x โ 0 โ โ i, (p i) x โ 0) โ T1Space E
This theorem states that for any given types ๐, E, and ฮน, where ๐ is a normed field, E is an additive commutative group and a ๐-module, and at least one element exists in ฮน. If E is a topological space and ๐, E, ฮน form a family of seminorms p associated with E, then if the seminorms satisfy the `WithSeminorms` property and for every non-zero element x of E there exists an index i such that the application of the seminorm p at i to x is non-zero, it follows that E is a T1 space. A T1 space is a topological space where for every pair of distinct points, each has a neighborhood not containing the other point.
More concisely: If ๐ is a normed field, E is an additive commutative group and a ๐-module, and there exists an element in ฮน, with ๐, E, ฮน forming a family of seminorms p on E satisfying the `WithSeminors` property, and for each non-zero x in E there exists an i such that p(i)(x) โ 0, then E is a T1 topological space.
|
SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf
theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [t : TopologicalSpace E] [inst_4 : TopologicalAddGroup E]
(p : SeminormFamily ๐ E ฮน), WithSeminorms p โ t = โจ
i, UniformSpace.toTopologicalSpace
This theorem asserts that for any given type ๐, type E, type ฮน, any normed field over type ๐, any additively commutative group over type E, any module over type ๐ and type E, any nonempty type ฮน, and any topological space over type E that is also a topological addition group, and for any seminorm family 'p' on ๐ and E indexed by ฮน, a space is associated with the seminorms 'p' if and only if the topology of that space is equal to the infimum of the topologies induced by each seminorm in the family individually. In other words, the topology induced by a family of seminorms corresponds to the infimum of the topologies induced by each seminorm in the family considered separately.
More concisely: The topology of a normed vector space with respect to a family of seminorms is equal to the infimum of the topologies induced by each seminorm in the family.
|
WithSeminorms.congr
theorem WithSeminorms.congr :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} {ฮน' : Type u_9} [inst : Nonempty ฮน] [inst_1 : Nonempty ฮน']
[inst_2 : NormedField ๐] [inst_3 : AddCommGroup E] [inst_4 : Module ๐ E] {p : SeminormFamily ๐ E ฮน}
{q : SeminormFamily ๐ E ฮน'} [t : TopologicalSpace E],
WithSeminorms p โ Seminorm.IsBounded p q LinearMap.id โ Seminorm.IsBounded q p LinearMap.id โ WithSeminorms q
In the realm of seminorms, the theorem `WithSeminorms.congr` states the following: Given two families of seminorms `p` and `q` on the same space, if each seminorm `p i` is bounded by some linear combination of a finite subset of `q`, and vice versa, then the topologies generated by `p` and `q` are equivalent. In this context, the boundedness of a seminorm is formulated as `Seminorm.IsBounded q p LinearMap.id` and its inverse. Rather than stating this as an equality of topologies, it is expressed in a more practical form: if the topology can be described with the seminorms `p`, and the boundedness conditions are satisfied, then the topology can also be described with the seminorms `q`.
More concisely: If two families of seminorms on the same vector space have each seminorm in one family bounded by a linear combination of a finite subset of seminorms in the other family, and vice versa, then the topologies generated by both families are equal.
|
SeminormFamily.basisSets_iff
theorem SeminormFamily.basisSets_iff :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] (p : SeminormFamily ๐ E ฮน) {U : Set E},
U โ p.basisSets โ โ i r, 0 < r โง U = (i.sup p).ball 0 r
The theorem `SeminormFamily.basisSets_iff` states that for any normed field `๐`, additive commutative group `E`, and type `ฮน`, given a seminorm family `p` and a set `U` of type `E`, `U` is in the basis sets of the seminorm family `p` if and only if there exist `i` and `r` such that `r` is greater than 0 and `U` is equal to the ball of radius `r` at 0 with respect to the supremum of the seminorms in `i` under the seminorm family `p`. In other words, a set `U` belongs to the basis sets of a seminorm family `p` if it can be represented as the ball in the seminorm space defined by the supremum of a subset of seminorms from `p`, with radius `r` and center at the origin.
More concisely: A set in a normed vector space is a basis set for a seminorm family if and only if it is equal to the ball centered at the origin with respect to the supremum of a subset of seminorms from the family.
|
Seminorm.bound_of_continuous_normedSpace
theorem Seminorm.bound_of_continuous_normedSpace :
โ {๐ : Type u_1} {F : Type u_6} [inst : NontriviallyNormedField ๐] [inst_1 : SeminormedAddCommGroup F]
[inst_2 : NormedSpace ๐ F] (q : Seminorm ๐ F), Continuous โq โ โ C, 0 < C โง โ (x : F), q x โค C * โxโ
This theorem states that for a semi-normed space 'F' over a non-trivially normed field '๐', if 'q' is a continuous semi-norm on 'F', then 'q' is uniformly controlled by the norm. In other words, there exists a positive constant 'C' such that for every element 'x' in 'F', the value of 'q' at 'x' is less than or equal to 'C' times the norm of 'x'. The continuity of 'q' ensures that it is bounded on a ball of some radius 'ฮต'. By using the nontriviality of the norm, any element can be rescaled into an element of norm in the range '[ฮต/C, ฮต)', which then has a controlled output by 'q'. Consequently, the control of 'q' at the original element can be obtained by rescaling.
More concisely: Given a semi-normed space 'F' over a non-trivially normed field '๐' and a continuous semi-norm 'q' on 'F', there exists a constant 'C' such that for all 'x' in 'F', 'q(x) โค C ยท ||x||'.
|
WithSeminorms.tendsto_nhds'
theorem WithSeminorms.tendsto_nhds' :
โ {๐ : Type u_1} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ
โ (u : F โ E) {f : Filter F} (yโ : E),
Filter.Tendsto u f (nhds yโ) โ โ (s : Finset ฮน) (ฮต : โ), 0 < ฮต โ โแถ (x : F) in f, (s.sup p) (u x - yโ) < ฮต
This theorem, named `WithSeminorms.tendsto_nhds'`, establishes the relationship between the convergence of a function along filters and seminorms. Specifically, it states that for any normed field `๐`, any additive commutative group `E`, any module `E` over `๐`, and any nonempty type `ฮน`, given a family of seminorms `p` on `E` indexed by `ฮน` and satisfying the property of `WithSeminorms`, a function `u` from `F` to `E`, a filter `f` on `F`, and an element `yโ` of `E`, the function `u` tends to `yโ` along the filter `f` (expressed as `Filter.Tendsto u f (nhds yโ)`) if and only if for any finite set `s` of elements from `ฮน` and any real number `ฮต` greater than zero, eventually (expressed as `โแถ (x : F) in f`) for each element `x` of `F`, the supremum (expressed as `s.sup p`) of the values of the seminorms in `p` applied to `u x - yโ` is less than `ฮต`.
More concisely: For any normed field `๐`, additive commutative group `E` over `๐`, nonempty type `ฮน`, family of seminorms `p` on `E` satisfying `WithSeminorms`, function `u` from `F` to `E`, filter `f` on `F`, and element `yโ` of `E`, `Filter.Tendsto u f (nhds yโ)` if and only if for any finite set `s` of indices from `ฮน` and any `ฮต > 0`, `s.sup p (u x - yโ) < ฮต` for eventually all `x` in `F` with respect to `f`.
|
WithSeminorms.mem_nhds_iff
theorem WithSeminorms.mem_nhds_iff :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ โ (x : E) (U : Set E), U โ nhds x โ โ s, โ r > 0, (s.sup p).ball x r โ U
The theorem `WithSeminorms.mem_nhds_iff` states that, for any normed field `๐`, additive commutative group `E`, and an index type `ฮน`, assuming the existence of `E` as a module over `๐`, the existence of at least one element in `ฮน`, and the topological space `E`, if a family `p` of seminorms induces the topology of the space, then for any element `x` in `E` and any set `U` in `E`, `U` is a neighborhood of `x` if and only if there exists a seminorm `s` in the family `p` and a positive radius `r` such that the ball centered at `x` with radius `r` with respect to the supremum of `s` in the family `p` is contained within `U`.
More concisely: For any normed field ๐, additive commutative group E with topology induced by a family p of seminorms, an element x in E, and a set U in E, U is a neighborhood of x if and only if there exists a seminorm s in p and a positive radius r such that the open ball B(x,rโฅsโฅp) is contained in U.
|
WithSeminorms.toLocallyConvexSpace
theorem WithSeminorms.toLocallyConvexSpace :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : Nonempty ฮน] [inst_1 : NormedField ๐]
[inst_2 : NormedSpace โ ๐] [inst_3 : AddCommGroup E] [inst_4 : Module ๐ E] [inst_5 : Module โ E]
[inst_6 : IsScalarTower โ ๐ E] [inst_7 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ LocallyConvexSpace โ E
This theorem states that for any nonempty type ฮน, a normed field ๐, a type E that is an additive commutative group and a ๐-module as well as an โ-module, a topological space on E, and a scalar tower of โ, ๐, and E, if we have a family of seminorms p from the type ฮน to the seminorms on ๐ and E (denoted as `SeminormFamily ๐ E ฮน`), and if these seminorms satisfy the `WithSeminorms` property, then E is a locally convex space over โ. In simpler terms, it means that a certain kind of structures built using seminorms can give us a locally convex space, a key concept in the study of topological vector spaces.
More concisely: Given a nonempty type ฮน, a normed field ๐, an additive commutative group and ๐-module E also an โ-module, a topological space on E, and a scalar tower, if we have a family of seminorms p on ฮน satisfying the `WithSeminorms` property, then E is a locally convex space over โ.
|
WithSeminorms.separating_iff_T1
theorem WithSeminorms.separating_iff_T1 :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ ((โ (x : E), x โ 0 โ โ i, (p i) x โ 0) โ T1Space E)
The theorem `WithSeminorms.separating_iff_T1` states that for any given normed field `๐`, type `E` with an additive commutative group structure and a `๐`-module structure, type `ฮน`, and a topological space structure on `E`, a family of seminorms `p` on `E` with respect to `๐` and indexed by `ฮน` is separating if and only if it induces a T1 topology on `E`. This means that if for each non-zero element `x` of `E`, there exists an index `i` such that the `i`-th seminorm of `x` is non-zero, then the topological space `E` is a T1 space, and vice versa. A T1 space is a topological space where for every pair of distinct points, each has a neighborhood not containing the other.
More concisely: A family of seminorms on a normed vector space induces a T1 topology if and only if every non-zero element has a non-zero seminorm in the family.
|
SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf
theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [u : UniformSpace E] [inst_4 : UniformAddGroup E]
(p : SeminormFamily ๐ E ฮน), WithSeminorms p โ u = โจ
i, PseudoMetricSpace.toUniformSpace
This theorem states that for any type of field `๐` that is a normed field, a type `E` that forms an additive commutative group and is a module over `๐`, and an indexing type `ฮน`, if `E` is equipped with a uniform space structure and additive uniform group structure, then the uniform structure induced by a family of seminorms `p` on `E` is exactly the infimum of the uniform structures induced by each individual seminorm in the family. More formally, `WithSeminorms p` is true if and only if the uniform space `u` is equal to the infimum of the uniform spaces induced by the pseudo-metric space corresponding to each individual seminorm in the family `p`.
More concisely: For a normed field `๐`, module `E` over `๐` with additive commutative group and uniform space structure, and indexing type `ฮน`, the uniform structure on `E` induced by a family `p` of seminorms is the infimum of the uniform structures induced by each individual seminorm in `p`.
|
WithSeminorms.tendsto_nhds_atTop
theorem WithSeminorms.tendsto_nhds_atTop :
โ {๐ : Type u_1} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน}
[inst_5 : SemilatticeSup F] [inst_6 : Nonempty F],
WithSeminorms p โ
โ (u : F โ E) (yโ : E),
Filter.Tendsto u Filter.atTop (nhds yโ) โ
โ (i : ฮน) (ฮต : โ), 0 < ฮต โ โ xโ, โ (x : F), xโ โค x โ (p i) (u x - yโ) < ฮต
This theorem, `WithSeminorms.tendsto_nhds_atTop`, is about limits towards infinity in the context of seminorms. Specifically, given a normed field `๐`, an additive commutative group `E`, a module `E` over `๐`, an indexed family of seminorms `p` on `E`, a function `u` from some sup-semilattice `F` to `E`, and a point `yโ` in `E`, the function `u` converges to `yโ` as the input tends towards infinity (`Filter.Tendsto u Filter.atTop (nhds yโ)`) if and only if for any index `i` and any real number `ฮต` greater than zero, there exists some `xโ` in `F` such that for all `x` in `F` greater than or equal to `xโ`, the seminorm of `u(x) - yโ` is less than `ฮต`. The theorem establishes a characterization of function convergence in terms of seminorms.
More concisely: Given a normed field `๐`, a module `E` over `๐`, an indexed family of seminorms `p` on `E`, a function `u` from a sup-semilattice `F` to `E`, and a point `yโ` in `E`, the function `u` converges to `yโ` as `x` approaches infinity if and only if for every `ฮต > 0`, there exists an `xโ` such that `p(u(x) - yโ) < ฮต` for all `x โฅ xโ`.
|
WithSeminorms.isOpen_iff_mem_balls
theorem WithSeminorms.isOpen_iff_mem_balls :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ โ (U : Set E), IsOpen U โ โ x โ U, โ s, โ r > 0, (s.sup p).ball x r โ U
The theorem `WithSeminorms.isOpen_iff_mem_balls` states that in a given topological space induced by a family of seminorms, a set is open if and only if it contains seminorm balls around all of its points. More specifically, for any set `U` in the space, `U` is open if for every point `x` in `U`, there exists a seminorm `s` and a real number `r` greater than zero such that the ball around `x` with radius `r` with respect to the supremum of seminorm `s` is contained in `U`.
More concisely: A set in a topological space induced by a family of seminorms is open if and only if for every point in the set, there exists a seminorm and a positive real number such that the seminorm ball around that point with that radius is contained in the set.
|
Seminorm.continuous_from_bounded
theorem Seminorm.continuous_from_bounded :
โ {๐ : Type u_3} {๐โ : Type u_4} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} {ฮน' : Type u_9}
[inst : AddCommGroup E] [inst_1 : NormedField ๐] [inst_2 : Module ๐ E] [inst_3 : AddCommGroup F]
[inst_4 : NormedField ๐โ] [inst_5 : Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [inst_6 : RingHomIsometric ฯโโ]
[inst_7 : Nonempty ฮน] [inst_8 : Nonempty ฮน'] {p : SeminormFamily ๐ E ฮน} {q : SeminormFamily ๐โ F ฮน'}
{x : TopologicalSpace E},
WithSeminorms p โ
โ {x_1 : TopologicalSpace F},
WithSeminorms q โ โ (f : E โโโ[ฯโโ] F), Seminorm.IsBounded p q f โ Continuous โf
This theorem, `Seminorm.continuous_from_bounded`, states that for all types `๐`, `๐โ`, `E`, `F`, `ฮน`, `ฮน'` where `E` and `F` are additive commutative groups, `๐` and `๐โ` are normed fields, `E` and `F` are modules over `๐` and `๐โ` respectively, there is a ring homomorphism `ฯโโ` from `๐` to `๐โ` which is isometric, and `ฮน` and `ฮน'` are nonempty. Given a seminorm family `p` on `๐` and `E` indexed by `ฮน`, and a seminorm family `q` on `๐โ` and `F` indexed by `ฮน'`, if `E` and `F` are topological spaces equipped with the seminorms `p` and `q` respectively, then for any continuous linear map `f` from `E` to `F` (in the sense of seminorms) that is bounded with respect to the seminorm families `p` and `q`, `f` is also a continuous function in the topological sense.
More concisely: Given normed fields `๐` and `๐โ`, additive commutative groups `E` and `F`, modules over `๐` and `๐โ` respectively, a ring homomorphism `ฯโโ` from `๐` to `๐โ` that is isometric, and seminorm families `p` on `E` and `q` on `F`, if `E`, `F`, `f` (a continuous linear map), and `p`, `q` satisfy the stated conditions, then `f` is a continuous function from `(E, p)` to `(F, q)`.
|
Seminorm.bound_of_continuous
theorem Seminorm.bound_of_continuous :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NontriviallyNormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] {p : SeminormFamily ๐ E ฮน} [inst_3 : Nonempty ฮน] [t : TopologicalSpace E],
WithSeminorms p โ โ (q : Seminorm ๐ E), Continuous โq โ โ s C, C โ 0 โง q โค C โข s.sup p
The theorem `Seminorm.bound_of_continuous` states that for a topological vector space `E` over a `NontriviallyNormedField` ๐, if the topology of `E` is generated by a family of seminorms `p`, and there exists a seminorm `q` on `E` that is continuous, then `q` can be uniformly controlled by a finite number of seminorms from `p`. More specifically, there exists a finite subset `s` from the index set of `p` and a non-zero constant `C` such that `q` is less than or equal to `C` times the supremum of `p` on `s`.
More concisely: If a topological vector space over a nontrivially normed field is generated by a family of seminorms and has a continuous seminorm, then there exists a finite subset of seminorms and a constant such that the continuous seminorm is dominated by the supremum of those seminorms on the subset.
|
norm_withSeminorms
theorem norm_withSeminorms :
โ (๐ : Type u_10) (E : Type u_11) [inst : NormedField ๐] [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E], WithSeminorms fun x => normSeminorm ๐ E
The theorem `norm_withSeminorms` states that for any normed field `๐` and any semi-normed additive commutative group `E` that is also a normed space over `๐`, the topology of the normed space `E` over `๐` is induced by the semi-norm given by the function `normSeminorm ๐ E`. This function assigns to any element of the space `E` the semi-norm derived from the norm of `E` as a group with respect to addition.
More concisely: The topology of a normed space over a normed field is induced by the semi-norm derived from its original norm.
|
WithSeminorms.separating_of_T1
theorem WithSeminorms.separating_of_T1 :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน}
[inst_5 : T1Space E], WithSeminorms p โ โ (x : E), x โ 0 โ โ i, (p i) x โ 0
The theorem `WithSeminorms.separating_of_T1` states that given a field `๐`, a type `E` with an addition operation and another operation that combines the elements of `๐` and `E`, an indexed type `ฮน`, where `E` has a topological space structure and `๐` is a normed field, if `p` is a family of seminorms on `E` inducing a Tโ topology (which means each singleton set is closed), then this family of seminorms is separating. In other words, for any non-zero element `x` in `E`, there exists an index `i` in `ฮน` such that the seminorm `p i` evaluated at `x` is not zero. This effectively means that no non-zero element in `E` is 'hidden' by the seminorms `p i` for all `i`.
More concisely: Given a normed field `๐`, a type `E` with a topology induced by a family `p` of separating seminorms, every non-zero element in `E` is separated from the origin by some seminorm `p_i` in the family.
|
WithSeminorms.tendsto_nhds
theorem WithSeminorms.tendsto_nhds :
โ {๐ : Type u_1} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : TopologicalSpace E] {p : SeminormFamily ๐ E ฮน},
WithSeminorms p โ
โ (u : F โ E) {f : Filter F} (yโ : E),
Filter.Tendsto u f (nhds yโ) โ โ (i : ฮน) (ฮต : โ), 0 < ฮต โ โแถ (x : F) in f, (p i) (u x - yโ) < ฮต
The theorem `WithSeminorms.tendsto_nhds` states that for a given normed field `๐`, an additive commutative group `E`, and a module `๐ E`, with `E` being a topological space, a seminorms family `p` on `๐` and `E`, and a function `u` from `F` to `E`, the function `u` tends to a limit `yโ` with respect to a filter `f` if and only if, for every element `i` of the index set ฮน, and for every real number `ฮต` greater than zero, the values of the seminorm `p i` on `(u x - yโ)` are eventually less than `ฮต` for `x` in the filter `f`. This condition expresses the notion of convergence in terms of seminorms.
More concisely: For a normed field ๐, an additive commutative group E with E being a topological space, a seminorms family p on ๐ and E, and a function u from F to E, the function u converges to yโ with respect to filter f if and only if, for every i in ฮน and every ฮต > 0, the seminorms p i of u(x) - yโ are eventually less than ฮต for x in f.
|
WithSeminorms.withSeminorms_eq
theorem WithSeminorms.withSeminorms_eq :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [t : TopologicalSpace E],
WithSeminorms p โ t = p.moduleFilterBasis.topology
This theorem, named `WithSeminorms.withSeminorms_eq`, states that for every type `๐` equipped with a norm field structure, type `E` equipped with an additive commutative group structure and a ๐-module structure, and type `ฮน` with at least one element, given a family `p` of seminorms indexed by `ฮน` on the vector space `E` over `๐`, and a topological space structure `t` on `E`, if `E` is equipped with the seminorms from `p` (`WithSeminorms p`), then the topology `t` is equal to the topology associated to the module filter basis induced by the filter basis of the seminorms in `p` (`ModuleFilterBasis.topology (SeminormFamily.moduleFilterBasis p)`). In simpler terms, this theorem expresses that the topological structure on a vector space with seminorms is given by the module filter basis induced by these seminorms.
More concisely: The topology on a normed vector space equipped with a family of seminorms is equal to the topology induced by the filter basis of these seminorms.
|
Seminorm.map_eq_zero_of_norm_zero
theorem Seminorm.map_eq_zero_of_norm_zero :
โ {๐ : Type u_1} {F : Type u_6} [inst : NontriviallyNormedField ๐] [inst_1 : SeminormedAddCommGroup F]
[inst_2 : NormedSpace ๐ F] (q : Seminorm ๐ F), Continuous โq โ โ {x : F}, โxโ = 0 โ q x = 0
This theorem states that in a semi-`NormedSpace`, if a `Seminorm` is continuous, it will map elements of the normed space, which have norm `0`, to `0`. More specifically, given any semi-`NormedSpace` (which is an additive group `F` over a field `๐`, where `๐` is a non-trivially normed field and `F` is equipped with a seminorm and a continuous scalar multiplication), for any continuous seminorm `q` and an element `x` of the space such that `x` has a norm of `0`, the value of `q` evaluated at `x` will be `0`.
More concisely: In a semi-NormedSpace over a non-trivially normed field, a continuous seminorm maps elements of norm 0 to 0.
|
WithSeminorms.equicontinuous_TFAE
theorem WithSeminorms.equicontinuous_TFAE :
โ {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน' : Type u_9} [inst : NontriviallyNormedField ๐]
[inst_1 : AddCommGroup E] [inst_2 : Module ๐ E] [inst_3 : NontriviallyNormedField ๐โ] [inst_4 : AddCommGroup F]
[inst_5 : Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [inst_6 : RingHomIsometric ฯโโ] [inst_7 : Nonempty ฮน'] {ฮบ : Type u_10}
{q : SeminormFamily ๐โ F ฮน'} [inst_8 : UniformSpace E] [inst_9 : UniformAddGroup E] [u : UniformSpace F]
[hu : UniformAddGroup F],
WithSeminorms q โ
โ [inst_10 : ContinuousSMul ๐ E] (f : ฮบ โ E โโโ[ฯโโ] F),
[EquicontinuousAt (DFunLike.coe โ f) 0, Equicontinuous (DFunLike.coe โ f),
UniformEquicontinuous (DFunLike.coe โ f),
โ (i : ฮน'), โ p, Continuous โp โง โ (k : ฮบ), (q i).comp (f k) โค p,
โ (i : ฮน'),
BddAbove (Set.range fun k => (q i).comp (f k)) โง Continuous (โจ k, โ((q i).comp (f k)))].TFAE
The theorem `WithSeminorms.equicontinuous_TFAE` describes a set of equivalent conditions for a family `f` of linear maps from one topological vector space `E` to another `F`, both over a `NontriviallyNormedField`. The vector space `F` is assumed to have a topology generated by a family of seminorms `q`. The equivalent conditions are:
* The family `f` is equicontinuous at `0` โ that is, for every entourage in `F`, there exists a neighborhood of `0` in `E` such that the image of any point in the neighborhood under any map in the family is close to the image of `0`.
* The family `f` is equicontinuous, meaning it is equicontinuous at every point in `E`.
* The family `f` is uniformly equicontinuous, meaning that for every entourage in `F`, there exists an entourage in `E` such that the image of any two close points under any map in the family are close.
* For each seminorm `q i`, the family of seminorms `(q i) โ (f k)` is bounded by a continuous seminorm on `E`.
* For each seminorm `q i`, the seminorm `โ k, (q i) โ (f k)` is well-defined and continuous.
These conditions completely characterize equicontinuity for linear maps from `E` to `F`, which can be particularly useful if all continuous seminorms on `E` can be determined. For instance, if both `E` and `F` are normed spaces, this theorem entails `NormedSpace.equicontinuous_TFAE`.
More concisely: A family of linear maps from a topological vector space to another with a topology generated by a family of seminorms is equicontinuous if and only if it is equicontinuous at 0, equicontinuous, uniformly equicontinuous, and for each seminorm on the range space, the corresponding composition with any map in the family is a bounded and continuous seminorm on the domain space.
|
NormedSpace.toLocallyConvexSpace'
theorem NormedSpace.toLocallyConvexSpace' :
โ (๐ : Type u_1) {E : Type u_5} [inst : NormedField ๐] [inst_1 : NormedSpace โ ๐]
[inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace ๐ E] [inst_4 : Module โ E] [inst : IsScalarTower โ ๐ E],
LocallyConvexSpace โ E
The theorem `NormedSpace.toLocallyConvexSpace'` states that for any normed field `๐` and any type `E` that is a seminormed add commutative group, a `๐`-normed space, a `โ`-module, and for which `โ` and `๐` act as scalars on `E`, `E` is a locally convex space over `โ`. Note that this is not made an instance as the field `๐` cannot be inferred. For a slightly weaker version that can be used as an instance, refer to `NormedSpace.toLocallyConvexSpace`.
More concisely: A seminormed add commutative group over a normed field that is also a normed space, an โ-module, and admits scalar multiplication by both โ and the normed field, is a locally convex space over โ.
|
WithSeminorms.first_countable
theorem WithSeminorms.first_countable :
โ {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [inst : NontriviallyNormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : Nonempty ฮน] [inst_4 : Countable ฮน] {p : SeminormFamily ๐ E ฮน}
[inst_5 : TopologicalSpace E], WithSeminorms p โ FirstCountableTopology E
This theorem, named 'WithSeminorms.first_countable', states that if the topology of a space is induced by a countable family of seminorms, then the topology is first countable. Specifically, for any non-trivially normed field ๐, any additive commutative group E and any type ฮน, assuming ๐ acts on E in the sense of module theory, ฮน is nonempty and countable, and we have a family of seminorms on E indexed by ฮน that induces a topological structure on E, then this topological structure is first countable. In a first countable space, every point has a countable basis of open neighborhoods, which means that we can do sequences and limits in the space, an important property in various branches of analysis.
More concisely: If a topology on a non-trivially normed module is induced by a countable family of seminorms, then the topology is first countable.
|