Topology induced by a family of seminorms #
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 ΞΉ] :
module_filter_basis π E
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
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), C β 0 β§ (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), C β 0 β§ (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.