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.

Main statements

• WithSeminorms.toLocallyConvexSpace: A space equipped with a family of seminorms is locally convex.
• WithSeminorms.firstCountable: 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 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

@[inline, reducible]

abbrev SeminormFamily (𝕜 : Type u_1) (E : Type u_5) (ι : Type u_8) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] : Type (max u_8 u_5)

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

Equations

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

def SeminormFamily.basisSets {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) : Set (Set E)

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

Equations

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

theorem SeminormFamily.basisSets_iff {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) {U : Set E} : U ∈ SeminormFamily.basisSets p ↔ ∃ i r x, U = Seminorm.ball (Finset.sup i p) 0 r

theorem SeminormFamily.basisSets_mem {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) (i : Finset ι) {r : ℝ} (hr : 0 < r) : Seminorm.ball (Finset.sup i p) 0 r ∈ SeminormFamily.basisSets p

theorem SeminormFamily.basisSets_singleton_mem {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) (i : ι) {r : ℝ} (hr : 0 < r) : Seminorm.ball (p i) 0 r ∈ SeminormFamily.basisSets p

theorem SeminormFamily.basisSets_nonempty {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) [Nonempty ι] : Set.Nonempty (SeminormFamily.basisSets p)

theorem SeminormFamily.basisSets_intersect {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) (U : Set E) (V : Set E) (hU : U ∈ SeminormFamily.basisSets p) (hV : V ∈ SeminormFamily.basisSets p) : ∃ z, z ∈ SeminormFamily.basisSets p ∧ z ⊆ U ∩ V

theorem SeminormFamily.basisSets_zero {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) (U : Set E) (hU : U ∈ SeminormFamily.basisSets p) : 0 ∈ U

theorem SeminormFamily.basisSets_add {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) (U : Set E) (hU : U ∈ SeminormFamily.basisSets p) : ∃ V, V ∈ SeminormFamily.basisSets p ∧ V + V ⊆ U

theorem SeminormFamily.basisSets_neg {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) (U : Set E) (hU' : U ∈ SeminormFamily.basisSets p) : ∃ V, V ∈ SeminormFamily.basisSets p ∧ V ⊆ (fun x => -x) ⁻¹' U

def SeminormFamily.addGroupFilterBasis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) [Nonempty ι] : AddGroupFilterBasis E

The addGroupFilterBasis induced by the filter basis Seminorm.basisSets.

Equations

• One or more equations did not get rendered due to their size.

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

theorem SeminormFamily.basisSets_smul {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) [Nonempty ι] (U : Set E) (hU : U ∈ SeminormFamily.basisSets p) : ∃ V, V ∈ nhds 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U

theorem SeminormFamily.basisSets_smul_left {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) [Nonempty ι] (x : 𝕜) (U : Set E) (hU : U ∈ SeminormFamily.basisSets p) : ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' U

def SeminormFamily.moduleFilterBasis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : SeminormFamily 𝕜 E ι) [Nonempty ι] : ModuleFilterBasis 𝕜 E

The moduleFilterBasis induced by the filter basis Seminorm.basisSets.

Equations

• One or more equations did not get rendered due to their size.

theorem SeminormFamily.filter_eq_iInf {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] (p : SeminormFamily 𝕜 E ι) : FilterBasis.filter AddGroupFilterBasis.toFilterBasis = ⨅ (i : ι), Filter.comap (↑(p i)) (nhds 0)

def Seminorm.IsBounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι : Type u_8} {ι' : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [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 C, Seminorm.comp (q i) f ≤ C • Finset.sup s p

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

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

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

structure WithSeminorms {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] (p : SeminormFamily 𝕜 E ι) [topology : TopologicalSpace E] : Prop

• topology_eq_withSeminorms : topology = ModuleFilterBasis.topology (SeminormFamily.moduleFilterBasis p)

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

theorem WithSeminorms.withSeminorms_eq {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) : t = ModuleFilterBasis.topology (SeminormFamily.moduleFilterBasis p)

theorem WithSeminorms.topologicalAddGroup {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : TopologicalAddGroup E

theorem WithSeminorms.continuousSMul {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : ContinuousSMul 𝕜 E

theorem WithSeminorms.hasBasis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : Filter.HasBasis (nhds 0) (fun s => s ∈ SeminormFamily.basisSets p) id

theorem WithSeminorms.hasBasis_zero_ball {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : Filter.HasBasis (nhds 0) (fun sr => 0 < sr.snd) fun sr => Seminorm.ball (Finset.sup sr.fst p) 0 sr.snd

theorem WithSeminorms.hasBasis_ball {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) {x : E} : Filter.HasBasis (nhds x) (fun sr => 0 < sr.snd) fun sr => Seminorm.ball (Finset.sup sr.fst p) x sr.snd

theorem WithSeminorms.mem_nhds_iff {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (x : E) (U : Set E) : U ∈ nhds x ↔ ∃ s r, r > 0 ∧ Seminorm.ball (Finset.sup s p) 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_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (U : Set E) : IsOpen U ↔ ∀ (x : E), x ∈ U → ∃ s r, r > 0 ∧ Seminorm.ball (Finset.sup s p) 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_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [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_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [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_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [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_1} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [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, ↑(Finset.sup s p) (u x - y₀) < ε

Convergence along filters for WithSeminorms.

Variant with Finset.sup.

theorem WithSeminorms.tendsto_nhds {𝕜 : Type u_1} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [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_1} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [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₀, ∀ (x : F), x₀ ≤ x → ↑(p i) (u x - y₀) < ε

Limit → ∞ for WithSeminorms.

theorem SeminormFamily.withSeminorms_of_nhds {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [t : TopologicalSpace E] [TopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) (h : nhds 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis) : WithSeminorms p

theorem SeminormFamily.withSeminorms_of_hasBasis {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [t : TopologicalSpace E] [TopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) (h : Filter.HasBasis (nhds 0) (fun s => s ∈ SeminormFamily.basisSets p) id) : WithSeminorms p

theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [t : TopologicalSpace E] [TopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ nhds 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (nhds 0)

theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [t : TopologicalSpace E] [TopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ t = ⨅ (i : ι), UniformSpace.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_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [t : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (i : ι) : Continuous ↑(p i)

theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [u : UniformSpace E] [UniformAddGroup 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_10) (E : Type u_11) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : WithSeminorms fun x => normSeminorm 𝕜 E

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

theorem WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] {s : Set E} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r

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

theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] {s : Set E} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r

theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded {𝕜 : Type u_1} {E : Type u_5} {G : Type u_7} {ι : Type u_8} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (f : G → E) {s : Set G} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (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} [AddCommGroup E] [NormedField 𝕝] [Module 𝕝 E] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] [Nonempty ι'] {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E] [TopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : ∀ (i : ι'), Continuous ↑(Seminorm.comp (q i) f)) : Continuous ↑f

theorem Seminorm.continuous_iff_continuous_comp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι' : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NontriviallyNormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [Nonempty ι'] {q : SeminormFamily 𝕜₂ F ι'} [TopologicalSpace E] [TopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) : Continuous ↑f ↔ ∀ (i : ι'), Continuous ↑(Seminorm.comp (q i) 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} [AddCommGroup E] [NormedField 𝕝] [Module 𝕝 E] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] [Nonempty ι] [Nonempty ι'] {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'} : ∀ {x : TopologicalSpace E}, WithSeminorms p → ∀ {x_1 : TopologicalSpace F}, WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Seminorm.IsBounded p q f → Continuous ↑f

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

theorem Seminorm.cont_normedSpace_to_withSeminorms {𝕝 : Type u_3} {𝕝₂ : Type u_4} {F : Type u_6} {ι : Type u_8} [NormedField 𝕝] [AddCommGroup F] [NormedField 𝕝₂] [Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [RingHomIsometric τ₁₂] [Nonempty ι] (E : Type u_10) [SeminormedAddCommGroup E] [NormedSpace 𝕝 E] [TopologicalSpace F] {q : ι → Seminorm 𝕝₂ F} (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : ∀ (i : ι), ∃ C, Seminorm.comp (q i) f ≤ C • normSeminorm 𝕝 E) : Continuous ↑f

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

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_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι' : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NontriviallyNormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [Nonempty ι'] {κ : Type u_10} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [UniformAddGroup E] [u : UniformSpace F] [hu : UniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) : UniformEquicontinuous (FunLike.coe ∘ f) ↔ ∀ (i : ι'), ∃ p, Continuous ↑p ∧ ∀ (k : κ), Seminorm.comp (q i) (f k) ≤ p

theorem WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι' : Type u_9} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NontriviallyNormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [Nonempty ι'] {κ : Type u_10} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [UniformAddGroup E] [u : UniformSpace F] [hu : UniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) : UniformEquicontinuous (FunLike.coe ∘ f) ↔ ∀ (i : ι'), BddAbove (Set.range fun k => Seminorm.comp (q i) (f k)) ∧ Continuous (⨆ (k : κ), ↑(Seminorm.comp (q i) (f k)))

theorem WithSeminorms.congr {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} {ι' : Type u_9} [Nonempty ι] [Nonempty ι'] [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_1} {E : Type u_5} {ι : Type u_8} [Nonempty ι] [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) : WithSeminorms fun s => Finset.sup s p

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

theorem WithSeminorms.congr_equiv {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} {ι' : Type u_9} [Nonempty ι] [Nonempty ι'] [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_zero {𝕜 : Type u_1} {F : Type u_6} [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.

theorem Seminorm.bound_of_continuous_normedSpace {𝕜 : Type u_1} {F : Type u_6} [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_1} {E : Type u_5} {ι : Type u_8} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [Nonempty ι] [t : TopologicalSpace E] (hp : WithSeminorms p) (q : Seminorm 𝕜 E) (hq : Continuous ↑q) : ∃ s C, C ≠ 0 ∧ q ≤ C • Finset.sup s 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_1} {E : Type u_5} {ι : Type u_8} [Nonempty ι] [NormedField 𝕜] [NormedSpace ℝ 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : LocallyConvexSpace ℝ E

theorem NormedSpace.toLocallyConvexSpace' (𝕜 : Type u_1) {E : Type u_5} [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_5} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : LocallyConvexSpace ℝ E

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

Equations

• @NormedSpace.toLocallyConvexSpace = @NormedSpace.toLocallyConvexSpace.proof_1

def SeminormFamily.comp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [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

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

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

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

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

theorem Inducing.withSeminorms {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_5} {F : Type u_6} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [TopologicalSpace F] [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : Inducing ↑f) : WithSeminorms (SeminormFamily.comp q f)

def SeminormFamily.sigma {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {κ : ι → Type u_10} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) : SeminormFamily 𝕜 E ((i : ι) × κ i)

(Disjoint) union of seminorm families.

Equations

• SeminormFamily.sigma p x = match x with | { fst := i, snd := k } => p i k

theorem withSeminorms_iInf {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {κ : ι → Type u_10} [Nonempty ((i : ι) × κ i)] [∀ (i : ι), Nonempty (κ i)] {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E} [∀ (i : ι), TopologicalAddGroup E] (hp : ∀ (i : ι), WithSeminorms (p i)) : WithSeminorms (SeminormFamily.sigma p)

theorem WithSeminorms.first_countable {𝕜 : Type u_1} {E : Type u_5} {ι : Type u_8} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ι] [Countable ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) : TopologicalSpace.FirstCountableTopology E

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