mathlib documentation

analysis.locally_convex.with_seminorms

Topology induced by a family of seminorms #

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) :
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) :
@[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), C β‰  0 ∧ 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), C β‰  0 ∧ (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 ΞΉ), 0 < C ∧ (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 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 ΞΉ) :
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 : ΞΉ) :
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 ΞΉ) :

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 ΞΉ) :

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) :
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) :

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) :
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.