mathlib3 documentation

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 #

Main statements #

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:

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.

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 ι) :
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 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm_family 𝕜 E ι) {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 𝕜] [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) :
(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 𝕜] [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) :
(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 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm_family 𝕜 E ι) (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 𝕜] [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
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) :
∀ᶠ (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 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm_family 𝕜 E ι) [nonempty ι] (U : set E) (hU : U p.basis_sets) :
(V : set 𝕜) (H : V nhds 0) (W : set E) (H : W add_group_filter_basis.to_filter_basis.sets), V W U
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) :
(V : set E) (H : V add_group_filter_basis.to_filter_basis.sets), 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 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm_family 𝕜 E ι) [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 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] (p : seminorm_family 𝕜 E ι) :
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.

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 𝕜] [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) :
seminorm.is_bounded p (λ (_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 𝕜] [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) :
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 𝕜] [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 ι') :
(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 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] (p : seminorm_family 𝕜 E ι) [t : topological_space E] :
Prop

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) :
(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 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] [topological_space E] {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) :
(nhds 0).has_basis (λ (sr : finset ι × ), 0 < sr.snd) (λ (sr : finset ι × ), (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 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] [topological_space E] {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) {x : E} :
(nhds x).has_basis (λ (sr : finset ι × ), 0 < sr.snd) (λ (sr : finset ι × ), (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 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] [topological_space E] {p : seminorm_family 𝕜 E ι} (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 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] [topological_space E] {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) (U : set E) :
is_open U (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 𝕜] [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)) :

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

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) :
filter.tendsto u f (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 𝕜] [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) :
filter.tendsto u f (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 𝕜] [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) :
filter.tendsto u filter.at_top (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_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 ι) :
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 : ι) :

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.

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) :
bornology.is_vonN_bounded 𝕜 s (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} [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) :
bornology.is_vonN_bounded 𝕜 (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} [nontrivially_normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] {p : seminorm_family 𝕜 E ι} [topological_space E] {s : set E} (hp : with_seminorms p) :
bornology.is_vonN_bounded 𝕜 s (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} [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) :
bornology.is_vonN_bounded 𝕜 (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} [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) :

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 𝕜] [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.

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 𝕜] [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) :
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 𝕜] [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) :
(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 𝕜] [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) :
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) :

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