# mathlib3documentation

analysis.locally_convex.with_seminorms

# 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 map f : E →ₗ[𝕜] F is bounded iff every seminorm in F can be bounded by a finite number of seminorms in E.

## 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 map f : E →ₗ[𝕜] F is 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_bounded
• with_seminorms.is_vonN_bounded_iff_seminorm_bounded
• with_seminorms.image_is_vonN_bounded_iff_finset_seminorm_bounded
• with_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 𝕜] [ 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 𝕜] [ E] (p : ι) :
set (set E)

The sets of a filter basis for the neighborhood filter of 0.

Equations
theorem seminorm_family.basis_sets_iff {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) {U : set E} :
U p.basis_sets (i : finset ι) (r : ) (hr : 0 < r), U = (i.sup p).ball 0 r
theorem seminorm_family.basis_sets_mem {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) (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 𝕜] [ E] (p : ι) (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 𝕜] [ E] (p : ι) [nonempty ι] :
theorem seminorm_family.basis_sets_intersect {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) (U V : set E) (hU : U p.basis_sets) (hV : V p.basis_sets) :
(z : set E) (H : z p.basis_sets), z U V
theorem seminorm_family.basis_sets_zero {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) (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 𝕜] [ E] (p : ι) (U : set E) (hU : U p.basis_sets) :
(V : set E) (H : V p.basis_sets), V + V U
theorem seminorm_family.basis_sets_neg {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) (U : set E) (hU' : U p.basis_sets) :
(V : set E) (H : V p.basis_sets), V (λ (x : E), -x) ⁻¹' U
@[protected]
def seminorm_family.add_group_filter_basis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) [nonempty ι] :

The add_group_filter_basis induced by the filter basis seminorm_basis_zero.

Equations
theorem seminorm_family.basis_sets_smul_right {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) (v : E) (U : set E) (hU : U p.basis_sets) :
∀ᶠ (x : 𝕜) in nhds 0, x v U
theorem seminorm_family.basis_sets_smul {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) [nonempty ι] (U : set E) (hU : U p.basis_sets) :
(V : set 𝕜) (H : V nhds 0) (W : set E) (H : , V W U
theorem seminorm_family.basis_sets_smul_left {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) [nonempty ι] (x : 𝕜) (U : set E) (hU : U p.basis_sets) :
(V : set E) (H : , V (λ (y : E), x y) ⁻¹' U
@[protected]
def seminorm_family.module_filter_basis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] (p : ι) [nonempty ι] :

The module_filter_basis induced by the filter basis seminorm_basis_zero.

Equations
theorem seminorm_family.filter_eq_infi {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [nonempty ι] (p : ι) :
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 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] (p : ι E) (q : ι' seminorm 𝕜₂ F) (f : E →ₛₗ[σ₁₂] F) :
Prop

The proposition that a linear map is bounded between spaces with families of seminorms.

Equations
theorem seminorm.is_bounded_const {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [normed_field 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] (ι' : Type u_3) [nonempty ι'] {p : ι E} {q : seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
(λ (_x : ι'), q) f (s : finset ι) (C : nnreal), q.comp f C s.sup p
theorem seminorm.const_is_bounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι' : Type u_9} [normed_field 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] (ι : Type u_3) [nonempty ι] {p : E} {q : ι' seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
seminorm.is_bounded (λ (_x : ι), p) q f (i : ι'), (C : nnreal), (q i).comp f C p
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 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] {p : ι E} {q : ι' seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F} (hf : f) (s' : finset ι') :
(C : nnreal) (s : finset ι), (s'.sup q).comp f C s.sup p
structure with_seminorms {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [nonempty ι] (p : ι) [t : topological_space E] :
Prop
• topology_eq_with_seminorms :

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 𝕜] [ E] [nonempty ι] {p : ι} [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 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) :
theorem with_seminorms.has_basis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) :
(nhds 0).has_basis (λ (s : set E), s p.basis_sets) id
theorem with_seminorms.has_basis_zero_ball {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) :
(nhds 0).has_basis (λ (sr : × ), 0 < sr.snd) (λ (sr : × ), (sr.fst.sup p).ball 0 sr.snd)
theorem with_seminorms.has_basis_ball {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) {x : E} :
(nhds x).has_basis (λ (sr : × ), 0 < sr.snd) (λ (sr : × ), (sr.fst.sup p).ball x sr.snd)
theorem with_seminorms.mem_nhds_iff {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) (x : E) (U : set E) :
U nhds x (s : finset ι) (r : ) (H : r > 0), (s.sup p).ball x r U

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 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) (U : set E) :
(x : E), x U ( (s : finset ι) (r : ) (H : r > 0), (s.sup p).ball x r U)

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 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) (h : (x : E), x 0 ( (i : ι), (p i) x 0)) :

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 𝕜] [ E] [nonempty ι] {p : ι} [t1_space E] (hp : with_seminorms p) (x : E) (hx : x 0) :
(i : ι), (p i) 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 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) :
( (x : E), x 0 ( (i : ι), (p i) x 0))

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 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) (u : F E) {f : filter F} (y₀ : E) :
(nhds y₀) (s : finset ι) (ε : ), 0 < ε (∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε)

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 𝕜] [ E] [nonempty ι] {p : ι} (hp : with_seminorms p) (u : F E) {f : filter F} (y₀ : E) :
(nhds y₀) (i : ι) (ε : ), 0 < ε (∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε)

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 𝕜] [ E] [nonempty ι] {p : ι} [nonempty F] (hp : with_seminorms p) (u : F E) (y₀ : E) :
(nhds y₀) (i : ι) (ε : ), 0 < ε ( (x₀ : F), (x : F), x₀ x (p i) (u x - y₀) < ε)

Limit → ∞ for with_seminorms.

theorem seminorm_family.with_seminorms_of_nhds {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [t : topological_space E] [nonempty ι] (p : ι)  :
theorem seminorm_family.with_seminorms_of_has_basis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [t : topological_space E] [nonempty ι] (p : ι) (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 𝕜] [ E] [t : topological_space E] [nonempty ι] (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} [t : topological_space E] [nonempty ι] [ E] {p : ι} (hp : with_seminorms p) (i : ι) :
theorem seminorm_family.with_seminorms_iff_topological_space_eq_infi {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [normed_field 𝕜] [ E] [t : topological_space E] [nonempty ι] (p : ι) :
t =

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 𝕜] [ E] [nonempty ι] [u : uniform_space E] (p : ι) :
u =

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 𝕜] [ E] :
with_seminorms (λ (_x : fin 1), 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} [ E] [nonempty ι] {p : ι} {s : set E} (hp : with_seminorms p) :
(I : finset ι), (r : ) (hr : 0 < r), (x : E), x s (I.sup p) x < r
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} [ E] [nonempty ι] {p : ι} (f : G E) {s : set G} (hp : with_seminorms p) :
(f '' s) (I : finset ι), (r : ) (hr : 0 < r), (x : G), x s (I.sup p) (f x) < r
theorem with_seminorms.is_vonN_bounded_iff_seminorm_bounded {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [ E] [nonempty ι] {p : ι} {s : set E} (hp : with_seminorms p) :
(i : ι), (r : ) (hr : 0 < r), (x : E), x s (p i) x < r
theorem with_seminorms.image_is_vonN_bounded_iff_seminorm_bounded {𝕜 : Type u_1} {E : Type u_5} {G : Type u_7} {ι : Type u_8} [ E] [nonempty ι] {p : ι} (f : G E) {s : set G} (hp : with_seminorms p) :
(f '' s) (i : ι), (r : ) (hr : 0 < r), (x : G), x s (p i) (f x) < r
theorem seminorm.continuous_of_continuous_comp {𝕝 : Type u_3} {𝕝₂ : Type u_4} {E : Type u_5} {F : Type u_6} {ι' : Type u_9} [normed_field 𝕝] [ E] [normed_field 𝕝₂] [module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [ring_hom_isometric τ₁₂] [nonempty ι'] {q : 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} [ E] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] [nonempty ι'] {q : F ι'} (hq : with_seminorms q) (f : E →ₛₗ[σ₁₂] 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} [normed_field 𝕝] [ E] [normed_field 𝕝₂] [module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [ring_hom_isometric τ₁₂] [nonempty ι] [nonempty ι'] {p : ι} {q : F ι'} (hp : with_seminorms p) (hq : with_seminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : f) :
theorem seminorm.cont_with_seminorms_normed_space {𝕝 : Type u_3} {𝕝₂ : Type u_4} {E : Type u_5} {ι : Type u_8} [normed_field 𝕝] [ E] [normed_field 𝕝₂] {τ₁₂ : 𝕝 →+* 𝕝₂} [ring_hom_isometric τ₁₂] [nonempty ι] (F : Type u_1) [ F] {p : ι E} (hp : with_seminorms p) (f : E →ₛₗ[τ₁₂] F) (hf : (s : finset ι) (C : nnreal), 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 𝕝] [normed_field 𝕝₂] [module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [ring_hom_isometric τ₁₂] [nonempty ι] (E : Type u_1) [ E] {q : ι seminorm 𝕝₂ F} (hq : with_seminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : (i : ι), (C : nnreal), (q i).comp f C ) :
theorem with_seminorms.to_locally_convex_space {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [nonempty ι] [normed_field 𝕜] [ 𝕜] [ E] [ E] [ E] {p : ι} (hp : with_seminorms p) :
theorem normed_space.to_locally_convex_space' (𝕜 : Type u_1) {E : Type u_5} [normed_field 𝕜] [ 𝕜] [ E] [ E] [ E] :

Not an instance since 𝕜 can't be inferred. See normed_space.to_locally_convex_space for a slightly weaker instance version.

@[protected, instance]

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 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] (q : F ι) (f : E →ₛₗ[σ₁₂] F) :
ι

The family of seminorms obtained by composing each seminorm by a linear map.

Equations
theorem seminorm_family.comp_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [normed_field 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] (q : F ι) (i : ι) (f : E →ₛₗ[σ₁₂] F) :
q.comp f i = (q i).comp 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 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] (q : F ι) (s : finset ι) (f : E →ₛₗ[σ₁₂] F) :
(s.sup q).comp f = s.sup (q.comp 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 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] [hι : nonempty ι] {q : F ι} (hq : with_seminorms q) (f : E →ₛₗ[σ₁₂] F) :
theorem inducing.with_seminorms {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [normed_field 𝕜] [ E] [normed_field 𝕜₂] [module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] [hι : nonempty ι] {q : F ι} (hq : with_seminorms q) {f : E →ₛₗ[σ₁₂] F} (hf : inducing f) :
theorem with_seminorms.first_countable {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [ E] [nonempty ι] [countable ι] {p : ι} (hp : with_seminorms p) :

If the topology of a space is induced by a countable family of seminorms, then the topology is first countable.