Topology induced by a family of seminorms

Main definitions

• SeminormFamily.basisSets: The set of open seminorm balls for a family of seminorms.
• SeminormFamily.moduleFilterBasis: A module filter basis formed by the open balls.
• Seminorm.IsBounded: A linear map f : E →ₗ[𝕜] F is bounded iff every seminorm in F can be bounded by a finite number of seminorms in E.
• WithSeminorms p, when p is a family of seminorms on E, is a proposition expressing that the (existing) topology on E is induced by the seminorms p.
• PolynormableSpace 𝕜 E is a class asserting that the (existing) topology on E is induced by some family of 𝕜-seminorms. If 𝕜 is RCLike, this is equivalent to LocallyConvexSpace 𝕜 E. The terminology is inspired by N. Bourbaki, Variétés différentielles et analytiques. However, unlike Bourbaki, we do not ask seminorms to be ultrametric when 𝕜 is ultrametric.

Main statements

• WithSeminorms.toLocallyConvexSpace: A space equipped with a family of seminorms is locally convex.
• WithSeminorms.firstCountable: A space is first countable if its 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 LinearMap.continuous_of_locally_bounded this gives general criterion for continuity.

• WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded
• WithSeminorms.isVonNBounded_iff_seminorm_bounded
• WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded
• WithSeminorms.image_isVonNBounded_iff_seminorm_bounded

Tags

seminorm, locally convex

@[reducible, inline]

abbrev SeminormFamily (R : Type u_1) (E : Type u_6) (ι : Type u_9) [SeminormedRing R] [AddCommGroup E] [Module R E] : Type (max u_9 u_6)

An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation.

Equations

• SeminormFamily R E ι = (ι → Seminorm R E)

def SeminormFamily.basisSets {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) : Set (Set E)

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

Equations

• p.basisSets = ⋃ (s : Finset ι), ⋃ (r : ℝ), ⋃ (_ : 0 < r), {(s.sup p).ball 0 r}

theorem SeminormFamily.basisSets_iff {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) {U : Set E} : U ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = (i.sup p).ball 0 r

theorem SeminormFamily.basisSets_mem {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (i : Finset ι) {r : ℝ} (hr : 0 < r) : (i.sup p).ball 0 r ∈ p.basisSets

theorem SeminormFamily.basisSets_singleton_mem {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (i : ι) {r : ℝ} (hr : 0 < r) : (p i).ball 0 r ∈ p.basisSets

theorem SeminormFamily.basisSets_univ_mem {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) : Set.univ ∈ p.basisSets

theorem SeminormFamily.basisSets_nonempty {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) : p.basisSets.Nonempty

theorem SeminormFamily.basisSets_intersect {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (U V : Set E) (hU : U ∈ p.basisSets) (hV : V ∈ p.basisSets) : ∃ z ∈ p.basisSets, z ⊆ U ∩ V

theorem SeminormFamily.basisSets_zero {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (U : Set E) (hU : U ∈ p.basisSets) : 0 ∈ U

theorem SeminormFamily.basisSets_add {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (U : Set E) (hU : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V + V ⊆ U

theorem SeminormFamily.basisSets_neg {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (U : Set E) (hU' : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) => -x) ⁻¹' U

def SeminormFamily.addGroupFilterBasis {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) : AddGroupFilterBasis E

The addGroupFilterBasis induced by the filter basis Seminorm.basisSets.

Equations

• p.addGroupFilterBasis = addGroupFilterBasisOfComm p.basisSets ⋯ ⋯ ⋯ ⋯ ⋯

theorem SeminormFamily.basisSets_smul_right {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (v : E) (U : Set E) (hU : U ∈ p.basisSets) : ∀ᶠ (x : R) in nhds 0, x • v ∈ U

theorem SeminormFamily.basisSets_smul {R : Type u_1} {E : Type u_6} {ι : Type u_9} [SeminormedRing R] [AddCommGroup E] [Module R E] (p : SeminormFamily R E ι) (U : Set E) (hU : U ∈ p.basisSets) : ∃ V ∈ nhds 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

theorem SeminormFamily.basisSets_smul_left {𝕜 : Type u_2} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup F] [Module 𝕜 F] (p : SeminormFamily 𝕜 F ι) (x : 𝕜) (U : Set F) (hU : U ∈ p.basisSets) : ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun (y : F) => x • y) ⁻¹' U

def SeminormFamily.moduleFilterBasis {𝕜 : Type u_2} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup F] [Module 𝕜 F] (p : SeminormFamily 𝕜 F ι) : ModuleFilterBasis 𝕜 F

The moduleFilterBasis induced by the filter basis Seminorm.basisSets.

Equations

• p.moduleFilterBasis = { toAddGroupFilterBasis := p.addGroupFilterBasis, smul' := ⋯, smul_left' := ⋯, smul_right' := ⋯ }

theorem SeminormFamily.filter_eq_iInf {𝕜 : Type u_2} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup F] [Module 𝕜 F] (p : SeminormFamily 𝕜 F ι) : p.moduleFilterBasis.filter = ⨅ (i : ι), Filter.comap (⇑(p i)) (nhds 0)

theorem SeminormFamily.basisSets_mem_nhds {𝕜 : Type u_11} {E : Type u_12} {ι : Type u_13} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (p : SeminormFamily 𝕜 E ι) (hp : ∀ (i : ι), Continuous ⇑(p i)) (U : Set E) (hU : U ∈ p.basisSets) : U ∈ nhds 0

If a family of seminorms is continuous, then their basis sets are neighborhoods of zero.

def Seminorm.IsBounded {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedRing 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (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

• Seminorm.IsBounded p q f = ∀ (i : ι'), ∃ (s : Finset ι) (C : NNReal), (q i).comp f ≤ C • s.sup p

theorem Seminorm.isBounded_const {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedRing 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (ι' : Type u_11) [Nonempty ι'] {p : ι → Seminorm 𝕜 E} {q : Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) : IsBounded p (fun (x : ι') => q) f ↔ ∃ (s : Finset ι) (C : NNReal), q.comp f ≤ C • s.sup p

theorem Seminorm.const_isBounded {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedRing 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (ι : Type u_11) [Nonempty ι] {p : Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) : IsBounded (fun (x : ι) => p) q f ↔ ∀ (i : ι'), ∃ (C : NNReal), (q i).comp f ≤ C • p

theorem Seminorm.isBounded_sup {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedRing 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {p : ι → Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F} (hf : IsBounded p q f) (s' : Finset ι') : ∃ (C : NNReal) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p

structure WithSeminorms {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) [topology : TopologicalSpace E] : Prop

The proposition that the topology of E is induced by a family of seminorms p.

• topology_eq_withSeminorms : topology = p.moduleFilterBasis.topology

class PolynormableSpace (𝕜 : Type u_2) (E : Type u_6) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [topology : TopologicalSpace E] : Prop

A topological vector space E is polynormable over 𝕜 if its topology is induced by some family of 𝕜-seminorms. Equivalently, its topology is induced by all its continuous seminorm.

If 𝕜 is RCLike, this is equivalent to LocallyConvexSpace 𝕜 E.

• withSeminorms' : WithSeminorms fun (p : { p : Seminorm 𝕜 E // Continuous ⇑p }) => ↑p

theorem WithSeminorms.withSeminorms_eq {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) : t = p.moduleFilterBasis.topology

theorem PolynormableSpace.withSeminorms (𝕜 : Type u_2) (E : Type u_6) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [PolynormableSpace 𝕜 E] : WithSeminorms fun (p : { p : Seminorm 𝕜 E // Continuous ⇑p }) => ↑p

theorem WithSeminorms.topologicalAddGroup {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : IsTopologicalAddGroup E

theorem WithSeminorms.continuousSMul {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : ContinuousSMul 𝕜 E

theorem WithSeminorms.hasBasis {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : (nhds 0).HasBasis (fun (s : Set E) => s ∈ p.basisSets) id

theorem WithSeminorms.hasBasis_zero_ball {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : (nhds 0).HasBasis (fun (sr : Finset ι × ℝ) => 0 < sr.2) fun (sr : Finset ι × ℝ) => (sr.1.sup p).ball 0 sr.2

theorem WithSeminorms.hasBasis_ball {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) {x : E} : (nhds x).HasBasis (fun (sr : Finset ι × ℝ) => 0 < sr.2) fun (sr : Finset ι × ℝ) => (sr.1.sup p).ball x sr.2

theorem WithSeminorms.mem_nhds_iff {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (x : E) (U : Set E) : U ∈ nhds x ↔ ∃ (s : Finset ι), ∃ 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 WithSeminorms.isOpen_iff_mem_balls {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (U : Set E) : IsOpen U ↔ ∀ x ∈ U, ∃ (s : Finset ι), ∃ 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 WithSeminorms.T1_of_separating {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), (p i) x ≠ 0) : T1Space E

A separating family of seminorms induces a T₁ topology.

theorem WithSeminorms.separating_of_T1 {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} [T1Space E] (hp : WithSeminorms p) (x : E) (hx : x ≠ 0) : ∃ (i : ι), (p i) x ≠ 0

A family of seminorms inducing a T₁ topology is separating.

theorem WithSeminorms.separating_iff_T1 {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : (∀ (x : E), x ≠ 0 → ∃ (i : ι), (p i) x ≠ 0) ↔ T1Space E

A family of seminorms is separating iff it induces a T₁ topology.

theorem WithSeminorms.tendsto_nhds' {𝕜 : Type u_2} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms 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 WithSeminorms.

Variant with Finset.sup.

theorem WithSeminorms.tendsto_nhds {𝕜 : Type u_2} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms 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 WithSeminorms.

theorem WithSeminorms.tendsto_nhds_atTop {𝕜 : Type u_2} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} [SemilatticeSup F] [Nonempty F] (hp : WithSeminorms p) (u : F → E) (y₀ : E) : Filter.Tendsto u Filter.atTop (nhds y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε

Limit → ∞ for WithSeminorms.

theorem SeminormFamily.withSeminorms_of_nhds {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) (h : nhds 0 = p.moduleFilterBasis.filter) : WithSeminorms p

theorem SeminormFamily.withSeminorms_of_hasBasis {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) (h : (nhds 0).HasBasis (fun (s : Set E) => s ∈ p.basisSets) id) : WithSeminorms p

theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ nhds 0 = ⨅ (i : ι), Filter.comap (⇑(p i)) (nhds 0)

theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ t = ⨅ (i : ι), PseudoMetricSpace.toUniformSpace.toTopologicalSpace

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 WithSeminorms p.

theorem WithSeminorms.continuous_seminorm {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [t : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (i : ι) : Continuous ⇑(p i)

theorem WithSeminorms.toPolynormableSpace {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [t : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : PolynormableSpace 𝕜 E

theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [u : UniformSpace E] [IsUniformAddGroup E] (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ u = ⨅ (i : ι), PseudoMetricSpace.toUniformSpace

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 WithSeminorms p.

theorem norm_withSeminorms (𝕜 : Type u_11) (E : Type u_12) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : WithSeminorms fun (x : Fin 1) => normSeminorm 𝕜 E

The topology of a NormedSpace 𝕜 E is induced by the seminorm normSeminorm 𝕜 E.

instance instPolynormableSpace {𝕜 : Type u_2} {E : Type u_6} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : PolynormableSpace 𝕜 E

A (semi-)normed space is polynormable.

theorem WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] {s : Set E} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

theorem WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded {𝕜 : Type u_2} {E : Type u_6} {G : Type u_8} {ι : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (f : G → E) {s : Set G} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) (f x) < r

theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] {s : Set E} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded {𝕜 : Type u_2} {E : Type u_6} {G : Type u_8} {ι : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (f : G → E) {s : Set G} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) (f x) < r

theorem withSeminorms_iff_mem_nhds_isVonNBounded {𝕜 : Type u_2} {E : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} : (WithSeminorms fun (x : Fin 1) => p) ↔ p.ball 0 1 ∈ nhds 0 ∧ Bornology.IsVonNBounded 𝕜 (p.ball 0 1)

In a topological vector space, the topology is generated by a single seminorm p iff the unit ball for this seminorm is a bounded neighborhood of 0.

theorem Seminorm.continuous_of_continuous_comp {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [AddCommGroup E] [NormedField 𝕝] [Module 𝕝 E] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)) : Continuous ⇑f

theorem Seminorm.continuous_iff_continuous_comp {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [AddCommGroup E] [NormedField 𝕝] [Module 𝕝 E] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) : Continuous ⇑f ↔ ∀ (i : ι'), Continuous ⇑((q i).comp f)

theorem Seminorm.continuous_from_bounded {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [AddCommGroup E] [NormedField 𝕝] [Module 𝕝 E] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'} {x✝ : TopologicalSpace E} (hp : WithSeminorms p) {x✝¹ : TopologicalSpace F} (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : IsBounded p q f) : Continuous ⇑f

theorem Seminorm.cont_withSeminorms_normedSpace {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {ι : Type u_9} [AddCommGroup E] [NormedField 𝕝] [Module 𝕝 E] [NormedField 𝕝₂] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] (F : Type u_11) [SeminormedAddCommGroup F] [NormedSpace 𝕝₂ F] [TopologicalSpace E] {p : ι → Seminorm 𝕝 E} (hp : WithSeminorms p) (f : E →ₛₗ[τ₁₂] F) (hf : ∃ (s : Finset ι) (C : NNReal), (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) : Continuous ⇑f

theorem Seminorm.cont_normedSpace_to_withSeminorms {𝕝 : Type u_4} {𝕝₂ : Type u_5} {F : Type u_7} {ι : Type u_9} [NormedField 𝕝] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] (E : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕝 E] [TopologicalSpace F] {q : ι → Seminorm 𝕝₂ F} (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : ∀ (i : ι), ∃ (C : NNReal), (q i).comp f ≤ C • normSeminorm 𝕝 E) : Continuous ⇑f

theorem WithSeminorms.equicontinuous_TFAE {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [hu : IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) : [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∀ (i : ι'), ∃ (p : Seminorm 𝕜 E), Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, ∀ (i : ι'), BddAbove (Set.range fun (k : κ) => (q i).comp (f k)) ∧ Continuous (⨆ (k : κ), ⇑((q i).comp (f k)))].TFAE

Let E and F be two topological vector spaces over a NontriviallyNormedField, and assume that the topology of F is generated by some family of seminorms q. For a family f of linear maps from E to F, the following are equivalent:

• f is equicontinuous at 0.
• f is equicontinuous.
• f is uniformly equicontinuous.
• For each q i, the family of seminorms k ↦ (q i) ∘ (f k) is bounded by some continuous seminorm p on E.
• For each q i, the seminorm ⊔ k, (q i) ∘ (f k) is well-defined and continuous.

In particular, if you can determine all continuous seminorms on E, that gives you a complete characterization of equicontinuity for linear maps from E to F. For example E and F are both normed spaces, you get NormedSpace.equicontinuous_TFAE.

theorem WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) : UniformEquicontinuous (DFunLike.coe ∘ f) ↔ ∀ (i : ι'), ∃ (p : Seminorm 𝕜 E), Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p

theorem WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) : UniformEquicontinuous (DFunLike.coe ∘ f) ↔ ∀ (i : ι'), BddAbove (Set.range fun (k : κ) => (q i).comp (f k)) ∧ Continuous (⨆ (k : κ), ⇑((q i).comp (f k)))

theorem WithSeminorms.congr {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} {ι' : Type u_10} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'} [t : TopologicalSpace E] (hp : WithSeminorms p) (hpq : Seminorm.IsBounded p q LinearMap.id) (hqp : Seminorm.IsBounded q p LinearMap.id) : WithSeminorms q

Two families of seminorms p and q on the same space generate the same topology if each p i is bounded by some C • Finset.sup s q and vice-versa.

We formulate these boundedness assumptions as Seminorm.IsBounded q p LinearMap.id (and vice-versa) to reuse the API. Furthermore, we don't actually state it as an equality of topologies but as a way to deduce WithSeminorms q from WithSeminorms p, since this should be more useful in practice.

theorem WithSeminorms.finset_sups {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) : WithSeminorms fun (s : Finset ι) => s.sup p

theorem WithSeminorms.partial_sups {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Preorder ι] [LocallyFiniteOrderBot ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) : WithSeminorms fun (i : ι) => (Finset.Iic i).sup p

theorem WithSeminorms.congr_equiv {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} {ι' : Type u_10} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) (e : ι' ≃ ι) : WithSeminorms (p ∘ ⇑e)

theorem Seminorm.map_eq_zero_of_norm_eq_zero {𝕜 : Type u_2} {F : Type u_7} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (q : Seminorm 𝕜 F) (hq : Continuous ⇑q) {x : F} (hx : ‖x‖ = 0) : q x = 0

In a semi-NormedSpace, a continuous seminorm is zero on elements of norm 0.

@[deprecated Seminorm.map_eq_zero_of_norm_eq_zero (since := "2025-11-15")]

theorem Seminorm.map_eq_zero_of_norm_zero {𝕜 : Type u_2} {F : Type u_7} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (q : Seminorm 𝕜 F) (hq : Continuous ⇑q) {x : F} (hx : ‖x‖ = 0) : q x = 0

Alias of Seminorm.map_eq_zero_of_norm_eq_zero.

---

In a semi-NormedSpace, a continuous seminorm is zero on elements of norm 0.

theorem Seminorm.bound_of_continuous_normedSpace {𝕜 : Type u_2} {F : Type u_7} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (q : Seminorm 𝕜 F) (hq : Continuous ⇑q) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖

Let F be a semi-NormedSpace over a NontriviallyNormedField, and let q be a seminorm on F. If q is continuous, then it is uniformly controlled by the norm, that is there is some C > 0 such that ∀ x, q x ≤ C * ‖x‖. The continuity ensures boundedness on a ball of some radius ε. The nontriviality of the norm is then used to rescale any element into an element of norm in [ε/C, ε[, thus with a controlled image by q. The control of q at the original element follows by rescaling.

theorem Seminorm.bound_of_continuous {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) (q : Seminorm 𝕜 E) (hq : Continuous ⇑q) : ∃ (s : Finset ι) (C : NNReal), C ≠ 0 ∧ q ≤ C • s.sup p

Let E be a topological vector space (over a NontriviallyNormedField) whose topology is generated by some family of seminorms p, and let q be a seminorm on E. If q is continuous, then it is uniformly controlled by finitely many seminorms of p, that is there is some finset s of the index set and some C > 0 such that q ≤ C • s.sup p.

theorem WithSeminorms.toLocallyConvexSpace {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [NormedSpace ℝ 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : LocallyConvexSpace ℝ E

@[instance 100]

instance instLocallyConvexSpaceRealOfPolynormableSpace {E : Type u_6} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [PolynormableSpace ℝ E] : LocallyConvexSpace ℝ E

A PolynormableSpace over ℝ is locally convex.

TODO: generalize to RCLike.

theorem NormedSpace.toLocallyConvexSpace' (𝕜 : Type u_2) {E : Type u_6} [NormedField 𝕜] [NormedSpace ℝ 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] : LocallyConvexSpace ℝ E

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

instance NormedSpace.toLocallyConvexSpace {E : Type u_6} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : LocallyConvexSpace ℝ E

See NormedSpace.toLocallyConvexSpace' for a slightly stronger version which is not an instance.

def SeminormFamily.comp {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (q : SeminormFamily 𝕜₂ F ι) (f : E →ₛₗ[σ₁₂] F) : SeminormFamily 𝕜 E ι

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

Equations

• q.comp f i = (q i).comp f

theorem SeminormFamily.comp_apply {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (q : SeminormFamily 𝕜₂ F ι) (i : ι) (f : E →ₛₗ[σ₁₂] F) : q.comp f i = (q i).comp f

theorem SeminormFamily.finset_sup_comp {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (q : SeminormFamily 𝕜₂ F ι) (s : Finset ι) (f : E →ₛₗ[σ₁₂] F) : (s.sup q).comp f = s.sup (q.comp f)

theorem LinearMap.withSeminorms_induced {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [TopologicalSpace F] {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) : WithSeminorms (q.comp f)

theorem Topology.IsInducing.withSeminorms {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [TopologicalSpace F] {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing ⇑f) : WithSeminorms (q.comp f)

def SeminormFamily.sigma {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {κ : ι → Type u_11} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) : SeminormFamily 𝕜 E ((i : ι) × κ i)

(Disjoint) union of seminorm families.

Equations

• SeminormFamily.sigma p ⟨i, k⟩ = p i k

theorem withSeminorms_iInf {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {κ : ι → Type u_11} {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E} (hp : ∀ (i : ι), WithSeminorms (p i)) : WithSeminorms (SeminormFamily.sigma p)

theorem withSeminorms_pi {𝕜 : Type u_2} {ι : Type u_9} [NormedField 𝕜] {κ : ι → Type u_11} {E : ι → Type u_12} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)} (hp : ∀ (i : ι), WithSeminorms (p i)) : WithSeminorms (SeminormFamily.sigma fun (i : ι) => (p i).comp (LinearMap.proj i))

theorem WithSeminorms.firstCountableTopology {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Countable ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) : FirstCountableTopology E

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