Topology induced by a family of seminorms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
seminorm_family.basis_sets: The set of open seminorm balls for a family of seminorms.seminorm_family.module_filter_basis: A module filter basis formed by the open balls.seminorm.is_bounded: A linear mapf : E →ₗ[𝕜] Fis bounded iff every seminorm inFcan be bounded by a finite number of seminorms inE.
Main statements #
with_seminorms.to_locally_convex_space: A space equipped with a family of seminorms is locally convex.with_seminorms.first_countable: A space is first countable if it's topology is induced by a countable family of seminorms.
Continuity of semilinear maps #
If E and F are topological vector space with the topology induced by a family of seminorms, then
we have a direct method to prove that a linear map is continuous:
seminorm.continuous_from_bounded: A bounded linear mapf : E →ₗ[𝕜] Fis continuous.
If the topology of a space E is induced by a family of seminorms, then we can characterize von
Neumann boundedness in terms of that seminorm family. Together with
linear_map.continuous_of_locally_bounded this gives general criterion for continuity.
with_seminorms.is_vonN_bounded_iff_finset_seminorm_boundedwith_seminorms.is_vonN_bounded_iff_seminorm_boundedwith_seminorms.image_is_vonN_bounded_iff_finset_seminorm_boundedwith_seminorms.image_is_vonN_bounded_iff_seminorm_bounded
Tags #
seminorm, locally convex
@[reducible]
def
seminorm_family
(𝕜 : Type u_1)
(E : Type u_5)
(ι : Type u_8)
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E] :
Type (max u_8 u_5)
An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation.
def
seminorm_family.basis_sets
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι) :
The sets of a filter basis for the neighborhood filter of 0.
theorem
seminorm_family.basis_sets_iff
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
{U : set E} :
theorem
seminorm_family.basis_sets_mem
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(i : finset ι)
{r : ℝ}
(hr : 0 < r) :
(i.sup p).ball 0 r ∈ p.basis_sets
theorem
seminorm_family.basis_sets_singleton_mem
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(i : ι)
{r : ℝ}
(hr : 0 < r) :
(p i).ball 0 r ∈ p.basis_sets
theorem
seminorm_family.basis_sets_nonempty
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
[nonempty ι] :
theorem
seminorm_family.basis_sets_intersect
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(U V : set E)
(hU : U ∈ p.basis_sets)
(hV : V ∈ p.basis_sets) :
theorem
seminorm_family.basis_sets_zero
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(U : set E)
(hU : U ∈ p.basis_sets) :
0 ∈ U
theorem
seminorm_family.basis_sets_add
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(U : set E)
(hU : U ∈ p.basis_sets) :
theorem
seminorm_family.basis_sets_neg
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(U : set E)
(hU' : U ∈ p.basis_sets) :
@[protected]
def
seminorm_family.add_group_filter_basis
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
[nonempty ι] :
The add_group_filter_basis induced by the filter basis seminorm_basis_zero.
Equations
- p.add_group_filter_basis = add_group_filter_basis_of_comm p.basis_sets _ _ _ _ _
theorem
seminorm_family.basis_sets_smul_right
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
(v : E)
(U : set E)
(hU : U ∈ p.basis_sets) :
theorem
seminorm_family.basis_sets_smul
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
[nonempty ι]
(U : set E)
(hU : U ∈ p.basis_sets) :
theorem
seminorm_family.basis_sets_smul_left
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
[nonempty ι]
(x : 𝕜)
(U : set E)
(hU : U ∈ p.basis_sets) :
@[protected]
def
seminorm_family.module_filter_basis
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm_family 𝕜 E ι)
[nonempty ι] :
The module_filter_basis induced by the filter basis seminorm_basis_zero.
Equations
- p.module_filter_basis = {to_add_group_filter_basis := p.add_group_filter_basis _inst_4, smul' := _, smul_left' := _, smul_right' := _}
theorem
seminorm_family.filter_eq_infi
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : seminorm_family 𝕜 E ι) :
add_group_filter_basis.to_filter_basis.filter = ⨅ (i : ι), filter.comap ⇑(p i) (nhds 0)
def
seminorm.is_bounded
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
{ι' : Type u_9}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(p : ι → seminorm 𝕜 E)
(q : ι' → seminorm 𝕜₂ F)
(f : E →ₛₗ[σ₁₂] F) :
Prop
The proposition that a linear map is bounded between spaces with families of seminorms.
theorem
seminorm.is_bounded_const
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(ι' : Type u_3)
[nonempty ι']
{p : ι → seminorm 𝕜 E}
{q : seminorm 𝕜₂ F}
(f : E →ₛₗ[σ₁₂] F) :
theorem
seminorm.const_is_bounded
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι' : Type u_9}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(ι : Type u_3)
[nonempty ι]
{p : seminorm 𝕜 E}
{q : ι' → seminorm 𝕜₂ F}
(f : E →ₛₗ[σ₁₂] F) :
theorem
seminorm.is_bounded_sup
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
{ι' : Type u_9}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{p : ι → seminorm 𝕜 E}
{q : ι' → seminorm 𝕜₂ F}
{f : E →ₛₗ[σ₁₂] F}
(hf : seminorm.is_bounded p q f)
(s' : finset ι') :
structure
with_seminorms
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : seminorm_family 𝕜 E ι)
[t : topological_space E] :
Prop
- topology_eq_with_seminorms : t = p.module_filter_basis.topology
The proposition that the topology of E is induced by a family of seminorms p.
theorem
with_seminorms.with_seminorms_eq
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
{p : seminorm_family 𝕜 E ι}
[t : topological_space E]
(hp : with_seminorms p) :
theorem
with_seminorms.topological_add_group
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p) :
theorem
with_seminorms.has_basis
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p) :
theorem
with_seminorms.has_basis_zero_ball
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p) :
theorem
with_seminorms.has_basis_ball
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p)
{x : E} :
theorem
with_seminorms.mem_nhds_iff
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p)
(x : E)
(U : set E) :
The x-neighbourhoods of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around x.
theorem
with_seminorms.is_open_iff_mem_balls
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p)
(U : set E) :
The open sets of a space whose topology is induced by a family of seminorms are exactly the sets which contain seminorm balls around all of their points.
theorem
with_seminorms.t1_of_separating
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p)
(h : ∀ (x : E), x ≠ 0 → (∃ (i : ι), ⇑(p i) x ≠ 0)) :
t1_space E
A separating family of seminorms induces a T₁ topology.
theorem
with_seminorms.separating_of_t1
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
[t1_space E]
(hp : with_seminorms p)
(x : E)
(hx : x ≠ 0) :
A family of seminorms inducing a T₁ topology is separating.
theorem
with_seminorms.separating_iff_t1
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p) :
A family of seminorms is separating iff it induces a T₁ topology.
theorem
with_seminorms.tendsto_nhds'
{𝕜 : Type u_1}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p)
(u : F → E)
{f : filter F}
(y₀ : E) :
Convergence along filters for with_seminorms.
Variant with finset.sup.
theorem
with_seminorms.tendsto_nhds
{𝕜 : Type u_1}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p)
(u : F → E)
{f : filter F}
(y₀ : E) :
Convergence along filters for with_seminorms.
theorem
with_seminorms.tendsto_nhds_at_top
{𝕜 : Type u_1}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[topological_space E]
{p : seminorm_family 𝕜 E ι}
[semilattice_sup F]
[nonempty F]
(hp : with_seminorms p)
(u : F → E)
(y₀ : E) :
Limit → ∞ for with_seminorms.
theorem
seminorm_family.with_seminorms_of_nhds
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[t : topological_space E]
[topological_add_group E]
[nonempty ι]
(p : seminorm_family 𝕜 E ι)
(h : nhds 0 = add_group_filter_basis.to_filter_basis.filter) :
theorem
seminorm_family.with_seminorms_of_has_basis
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[t : topological_space E]
[topological_add_group E]
[nonempty ι]
(p : seminorm_family 𝕜 E ι)
(h : (nhds 0).has_basis (λ (s : set E), s ∈ p.basis_sets) id) :
theorem
seminorm_family.with_seminorms_iff_nhds_eq_infi
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[t : topological_space E]
[topological_add_group E]
[nonempty ι]
(p : seminorm_family 𝕜 E ι) :
with_seminorms p ↔ nhds 0 = ⨅ (i : ι), filter.comap ⇑(p i) (nhds 0)
theorem
with_seminorms.continuous_seminorm
{𝕝 : Type u_3}
{E : Type u_5}
{ι : Type u_8}
[add_comm_group E]
[t : topological_space E]
[topological_add_group E]
[nonempty ι]
[nontrivially_normed_field 𝕝]
[module 𝕝 E]
[has_continuous_const_smul 𝕝 E]
{p : seminorm_family 𝕝 E ι}
(hp : with_seminorms p)
(i : ι) :
continuous ⇑(p i)
theorem
seminorm_family.with_seminorms_iff_topological_space_eq_infi
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[t : topological_space E]
[topological_add_group E]
[nonempty ι]
(p : seminorm_family 𝕜 E ι) :
with_seminorms p ↔ t = ⨅ (i : ι), uniform_space.to_topological_space
The topology induced by a family of seminorms is exactly the infimum of the ones induced by
each seminorm individually. We express this as a characterization of with_seminorms p.
theorem
seminorm_family.with_seminorms_iff_uniform_space_eq_infi
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[u : uniform_space E]
[uniform_add_group E]
(p : seminorm_family 𝕜 E ι) :
with_seminorms p ↔ u = ⨅ (i : ι), pseudo_metric_space.to_uniform_space
The uniform structure induced by a family of seminorms is exactly the infimum of the ones
induced by each seminorm individually. We express this as a characterization of
with_seminorms p.
theorem
norm_with_seminorms
(𝕜 : Type u_1)
(E : Type u_2)
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E] :
with_seminorms (λ (_x : fin 1), norm_seminorm 𝕜 E)
The topology of a normed_space 𝕜 E is induced by the seminorm norm_seminorm 𝕜 E.
theorem
with_seminorms.is_vonN_bounded_iff_finset_seminorm_bounded
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
{p : seminorm_family 𝕜 E ι}
[topological_space E]
{s : set E}
(hp : with_seminorms p) :
theorem
with_seminorms.image_is_vonN_bounded_iff_finset_seminorm_bounded
{𝕜 : Type u_1}
{E : Type u_5}
{G : Type u_7}
{ι : Type u_8}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
{p : seminorm_family 𝕜 E ι}
[topological_space E]
(f : G → E)
{s : set G}
(hp : with_seminorms p) :
theorem
with_seminorms.is_vonN_bounded_iff_seminorm_bounded
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
{p : seminorm_family 𝕜 E ι}
[topological_space E]
{s : set E}
(hp : with_seminorms p) :
theorem
with_seminorms.image_is_vonN_bounded_iff_seminorm_bounded
{𝕜 : Type u_1}
{E : Type u_5}
{G : Type u_7}
{ι : Type u_8}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
{p : seminorm_family 𝕜 E ι}
[topological_space E]
(f : G → E)
{s : set G}
(hp : with_seminorms p) :
theorem
seminorm.continuous_of_continuous_comp
{𝕝 : Type u_3}
{𝕝₂ : Type u_4}
{E : Type u_5}
{F : Type u_6}
{ι' : Type u_9}
[add_comm_group E]
[normed_field 𝕝]
[module 𝕝 E]
[add_comm_group F]
[normed_field 𝕝₂]
[module 𝕝₂ F]
{τ₁₂ : 𝕝 →+* 𝕝₂}
[ring_hom_isometric τ₁₂]
[nonempty ι']
{q : seminorm_family 𝕝₂ F ι'}
[topological_space E]
[topological_add_group E]
[topological_space F]
[topological_add_group F]
(hq : with_seminorms q)
(f : E →ₛₗ[τ₁₂] F)
(hf : ∀ (i : ι'), continuous ⇑((q i).comp f)) :
theorem
seminorm.continuous_iff_continuous_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι' : Type u_9}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nontrivially_normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[nonempty ι']
{q : seminorm_family 𝕜₂ F ι'}
[topological_space E]
[topological_add_group E]
[topological_space F]
[topological_add_group F]
[has_continuous_const_smul 𝕜₂ F]
(hq : with_seminorms q)
(f : E →ₛₗ[σ₁₂] F) :
continuous ⇑f ↔ ∀ (i : ι'), continuous ⇑((q i).comp f)
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}
[add_comm_group E]
[normed_field 𝕝]
[module 𝕝 E]
[add_comm_group F]
[normed_field 𝕝₂]
[module 𝕝₂ F]
{τ₁₂ : 𝕝 →+* 𝕝₂}
[ring_hom_isometric τ₁₂]
[nonempty ι]
[nonempty ι']
{p : seminorm_family 𝕝 E ι}
{q : seminorm_family 𝕝₂ F ι'}
[topological_space E]
[topological_add_group E]
(hp : with_seminorms p)
[topological_space F]
[topological_add_group F]
(hq : with_seminorms q)
(f : E →ₛₗ[τ₁₂] F)
(hf : seminorm.is_bounded p q f) :
theorem
seminorm.cont_with_seminorms_normed_space
{𝕝 : Type u_3}
{𝕝₂ : Type u_4}
{E : Type u_5}
{ι : Type u_8}
[add_comm_group E]
[normed_field 𝕝]
[module 𝕝 E]
[normed_field 𝕝₂]
{τ₁₂ : 𝕝 →+* 𝕝₂}
[ring_hom_isometric τ₁₂]
[nonempty ι]
(F : Type u_1)
[seminormed_add_comm_group F]
[normed_space 𝕝₂ F]
[uniform_space E]
[uniform_add_group E]
{p : ι → seminorm 𝕝 E}
(hp : with_seminorms p)
(f : E →ₛₗ[τ₁₂] F)
(hf : ∃ (s : finset ι) (C : nnreal), (norm_seminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
theorem
seminorm.cont_normed_space_to_with_seminorms
{𝕝 : Type u_3}
{𝕝₂ : Type u_4}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕝]
[add_comm_group F]
[normed_field 𝕝₂]
[module 𝕝₂ F]
{τ₁₂ : 𝕝 →+* 𝕝₂}
[ring_hom_isometric τ₁₂]
[nonempty ι]
(E : Type u_1)
[seminormed_add_comm_group E]
[normed_space 𝕝 E]
[uniform_space F]
[uniform_add_group F]
{q : ι → seminorm 𝕝₂ F}
(hq : with_seminorms q)
(f : E →ₛₗ[τ₁₂] F)
(hf : ∀ (i : ι), ∃ (C : nnreal), (q i).comp f ≤ C • norm_seminorm 𝕝 E) :
theorem
with_seminorms.to_locally_convex_space
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[nonempty ι]
[normed_field 𝕜]
[normed_space ℝ 𝕜]
[add_comm_group E]
[module 𝕜 E]
[module ℝ E]
[is_scalar_tower ℝ 𝕜 E]
[topological_space E]
[topological_add_group E]
{p : seminorm_family 𝕜 E ι}
(hp : with_seminorms p) :
theorem
normed_space.to_locally_convex_space'
(𝕜 : Type u_1)
{E : Type u_5}
[normed_field 𝕜]
[normed_space ℝ 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[module ℝ E]
[is_scalar_tower ℝ 𝕜 E] :
Not an instance since 𝕜 can't be inferred. See normed_space.to_locally_convex_space for a
slightly weaker instance version.
@[protected, instance]
def
normed_space.to_locally_convex_space
{E : Type u_5}
[seminormed_add_comm_group E]
[normed_space ℝ E] :
See normed_space.to_locally_convex_space' for a slightly stronger version which is not an
instance.
def
seminorm_family.comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(q : seminorm_family 𝕜₂ F ι)
(f : E →ₛₗ[σ₁₂] F) :
seminorm_family 𝕜 E ι
The family of seminorms obtained by composing each seminorm by a linear map.
theorem
seminorm_family.comp_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(q : seminorm_family 𝕜₂ F ι)
(i : ι)
(f : E →ₛₗ[σ₁₂] F) :
theorem
seminorm_family.finset_sup_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(q : seminorm_family 𝕜₂ F ι)
(s : finset ι)
(f : E →ₛₗ[σ₁₂] F) :
theorem
linear_map.with_seminorms_induced
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[topological_space F]
[topological_add_group F]
[hι : nonempty ι]
{q : seminorm_family 𝕜₂ F ι}
(hq : with_seminorms q)
(f : E →ₛₗ[σ₁₂] F) :
with_seminorms (q.comp f)
theorem
inducing.with_seminorms
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_5}
{F : Type u_6}
{ι : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[normed_field 𝕜₂]
[add_comm_group F]
[module 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[topological_space F]
[topological_add_group F]
[hι : nonempty ι]
{q : seminorm_family 𝕜₂ F ι}
(hq : with_seminorms q)
[topological_space E]
{f : E →ₛₗ[σ₁₂] F}
(hf : inducing ⇑f) :
with_seminorms (q.comp f)
theorem
with_seminorms.first_countable
{𝕜 : Type u_1}
{E : Type u_5}
{ι : Type u_8}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
[countable ι]
{p : seminorm_family 𝕜 E ι}
[uniform_space E]
[uniform_add_group E]
(hp : with_seminorms p) :
If the topology of a space is induced by a countable family of seminorms, then the topology is first countable.