# 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

@[reducible, inline]
abbrev SeminormFamily (๐ : Type u_1) (E : Type u_5) (ฮน : Type u_8) [NormedField ๐] [] [Module ๐ E] :
Type (max u_8 u_5)

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

Equations
Instances For
def SeminormFamily.basisSets {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ 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}
Instances For
theorem SeminormFamily.basisSets_iff {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) {U : Set E} :
U โ p.basisSets โ โ (i : Finset ฮน) (r : โ), 0 < r โง U = (i.sup p).ball 0 r
theorem SeminormFamily.basisSets_mem {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (i : Finset ฮน) {r : โ} (hr : 0 < r) :
(i.sup p).ball 0 r โ p.basisSets
theorem SeminormFamily.basisSets_singleton_mem {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (i : ฮน) {r : โ} (hr : 0 < r) :
(p i).ball 0 r โ p.basisSets
theorem SeminormFamily.basisSets_nonempty {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) [Nonempty ฮน] :
p.basisSets.Nonempty
theorem SeminormFamily.basisSets_intersect {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (U : Set E) (V : Set E) (hU : U โ p.basisSets) (hV : V โ p.basisSets) :
โ z โ p.basisSets, z โ U โฉ V
theorem SeminormFamily.basisSets_zero {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (U : Set E) (hU : U โ p.basisSets) :
theorem SeminormFamily.basisSets_add {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (U : Set E) (hU : U โ p.basisSets) :
โ V โ p.basisSets, V + V โ U
theorem SeminormFamily.basisSets_neg {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (U : Set E) (hU' : U โ p.basisSets) :
โ V โ p.basisSets, V โ (fun (x : E) => -x) โปยน' U
def SeminormFamily.addGroupFilterBasis {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) [Nonempty ฮน] :

The addGroupFilterBasis induced by the filter basis Seminorm.basisSets.

Equations
Instances For
theorem SeminormFamily.basisSets_smul_right {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) (v : E) (U : Set E) (hU : U โ p.basisSets) :
โแถ  (x : ๐) in nhds 0, x โข v โ U
theorem SeminormFamily.basisSets_smul {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) [Nonempty ฮน] (U : Set E) (hU : U โ p.basisSets) :
โ V โ nhds 0, โ W โ AddGroupFilterBasis.toFilterBasis.sets, V โข W โ U
theorem SeminormFamily.basisSets_smul_left {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) [Nonempty ฮน] (x : ๐) (U : Set E) (hU : U โ p.basisSets) :
โ V โ AddGroupFilterBasis.toFilterBasis.sets, V โ (fun (y : E) => x โข y) โปยน' U
def SeminormFamily.moduleFilterBasis {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] (p : SeminormFamily ๐ E ฮน) [Nonempty ฮน] :
ModuleFilterBasis ๐ E

The moduleFilterBasis induced by the filter basis Seminorm.basisSets.

Equations
• p.moduleFilterBasis = { toAddGroupFilterBasis := p.addGroupFilterBasis, smul' := โฏ, smul_left' := โฏ, smul_right' := โฏ }
Instances For
theorem SeminormFamily.filter_eq_iInf {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] (p : SeminormFamily ๐ E ฮน) :
AddGroupFilterBasis.toFilterBasis.filter = โจ (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 ๐] [] [Module ๐ E] [NormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] (p : ฮน โ Seminorm ๐ E) (q : ฮน' โ Seminorm ๐โ F) (f : E โโโ[ฯโโ] F) :

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

Equations
Instances For
theorem Seminorm.isBounded_const {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] (ฮน' : Type u_10) [Nonempty ฮน'] {p : ฮน โ Seminorm ๐ E} {q : Seminorm ๐โ F} (f : E โโโ[ฯโโ] F) :
Seminorm.IsBounded p (fun (x : ฮน') => q) f โ โ (s : Finset ฮน) (C : NNReal), q.comp f โค C โข s.sup p
theorem Seminorm.const_isBounded {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน' : Type u_9} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [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 : NNReal), (q i).comp 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 ๐] [] [Module ๐ E] [NormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] {p : ฮน โ Seminorm ๐ E} {q : ฮน' โ Seminorm ๐โ F} {f : E โโโ[ฯโโ] F} (hf : ) (s' : Finset ฮน') :
โ (C : NNReal) (s : Finset ฮน), (s'.sup q).comp f โค C โข s.sup p
structure WithSeminorms {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] (p : SeminormFamily ๐ E ฮน) [topology : ] :

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

• topology_eq_withSeminorms : topology = p.moduleFilterBasis.topology
Instances For
theorem WithSeminorms.topology_eq_withSeminorms {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [topology : ] (self : ) :
topology = p.moduleFilterBasis.topology
theorem WithSeminorms.withSeminorms_eq {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [t : ] (hp : ) :
t = p.moduleFilterBasis.topology
theorem WithSeminorms.topologicalAddGroup {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) :
theorem WithSeminorms.continuousSMul {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) :
ContinuousSMul ๐ E
theorem WithSeminorms.hasBasis {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) :
(nhds 0).HasBasis (fun (s : Set E) => s โ p.basisSets) id
theorem WithSeminorms.hasBasis_zero_ball {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) :
(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_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) {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_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) (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_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) (U : Set E) :
โ โ 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_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) (h : โ (x : E), x โ  0 โ โ (i : ฮน), (p i) x โ  0) :

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 ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} [] (hp : ) (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 ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) :
(โ (x : E), x โ  0 โ โ (i : ฮน), (p i) x โ  0) โ

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 ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) (u : F โ E) {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_1} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} (hp : ) (u : F โ E) {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 ๐] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} [] [] (hp : ) (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_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [t : ] (p : SeminormFamily ๐ E ฮน) (h : nhds 0 = AddGroupFilterBasis.toFilterBasis.filter) :
theorem SeminormFamily.withSeminorms_of_hasBasis {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [t : ] (p : SeminormFamily ๐ E ฮน) (h : (nhds 0).HasBasis (fun (s : Set E) => s โ p.basisSets) id) :
theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [t : ] (p : SeminormFamily ๐ E ฮน) :
โ 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 ๐] [] [Module ๐ E] [Nonempty ฮน] [t : ] (p : SeminormFamily ๐ E ฮน) :
โ 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 ๐] [] [Module ๐ E] [Nonempty ฮน] [t : ] {p : SeminormFamily ๐ E ฮน} (hp : ) (i : ฮน) :
Continuous โ(p i)
theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [Nonempty ฮน] [u : ] [] (p : SeminormFamily ๐ E ฮน) :
โ 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 ๐] [NormedSpace ๐ E] :
WithSeminorms fun (x : Fin 1) => 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} [] [] [Module ๐ E] [Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [] {s : Set E} (hp : ) :
โ โ (I : Finset ฮน), โ r > 0, โ x โ s, (I.sup 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} [] [] [Module ๐ E] [Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [] (f : G โ E) {s : Set G} (hp : ) :
Bornology.IsVonNBounded ๐ (f '' s) โ โ (I : Finset ฮน), โ r > 0, โ x โ s, (I.sup p) (f x) < r
theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [] [] [Module ๐ E] [Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [] {s : Set E} (hp : ) :
โ โ (i : ฮน), โ r > 0, โ 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} [] [] [Module ๐ E] [Nonempty ฮน] {p : SeminormFamily ๐ E ฮน} [] (f : G โ E) {s : Set G} (hp : ) :
Bornology.IsVonNBounded ๐ (f '' s) โ โ (i : ฮน), โ r > 0, โ 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} [] [NormedField ๐] [Module ๐ E] [] [NormedField ๐โ] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน'] {q : SeminormFamily ๐โ F ฮน'} [] [] (hq : ) (f : E โโโ[ฯโโ] F) (hf : โ (i : ฮน'), Continuous โ((q i).comp 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} [] [] [Module ๐ E] [NontriviallyNormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน'] {q : SeminormFamily ๐โ F ฮน'} [] [] (hq : ) (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} [] [NormedField ๐] [Module ๐ E] [] [NormedField ๐โ] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน] [Nonempty ฮน'] {p : SeminormFamily ๐ E ฮน} {q : SeminormFamily ๐โ F ฮน'} :
โ {x : }, โ โ {x_1 : }, โ โ (f : E โโโ[ฯโโ] F), โ Continuous โf
theorem Seminorm.cont_withSeminorms_normedSpace {๐ : Type u_3} {๐โ : Type u_4} {E : Type u_5} {ฮน : Type u_8} [] [NormedField ๐] [Module ๐ E] [NormedField ๐โ] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน] (F : Type u_10) [NormedSpace ๐โ F] [] {p : ฮน โ Seminorm ๐ E} (hp : ) (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_3} {๐โ : Type u_4} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [NormedField ๐โ] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน] (E : Type u_10) [NormedSpace ๐ E] [] {q : ฮน โ Seminorm ๐โ F} (hq : ) (f : E โโโ[ฯโโ] F) (hf : โ (i : ฮน), โ (C : NNReal), (q i).comp 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} [] [] [Module ๐ E] [NontriviallyNormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน'] {ฮบ : Type u_10} {q : SeminormFamily ๐โ F ฮน'} [] [] [u : ] [hu : ] (hq : ) [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_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน' : Type u_9} [] [] [Module ๐ E] [NontriviallyNormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน'] {ฮบ : Type u_10} {q : SeminormFamily ๐โ F ฮน'} [] [] [u : ] [hu : ] (hq : ) [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_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน' : Type u_9} [] [] [Module ๐ E] [NontriviallyNormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [Nonempty ฮน'] {ฮบ : Type u_10} {q : SeminormFamily ๐โ F ฮน'} [] [] [u : ] [hu : ] (hq : ) [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_1} {E : Type u_5} {ฮน : Type u_8} {ฮน' : Type u_9} [Nonempty ฮน] [Nonempty ฮน'] [NormedField ๐] [] [Module ๐ E] {p : SeminormFamily ๐ E ฮน} {q : SeminormFamily ๐ E ฮน'} [t : ] (hp : ) (hpq : Seminorm.IsBounded p q LinearMap.id) (hqp : Seminorm.IsBounded q p LinearMap.id) :

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 ๐] [] [Module ๐ E] {p : SeminormFamily ๐ E ฮน} [] (hp : ) :
WithSeminorms fun (s : Finset ฮน) => s.sup p
theorem WithSeminorms.partial_sups {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [Nonempty ฮน] [NormedField ๐] [] [Module ๐ E] [Preorder ฮน] {p : SeminormFamily ๐ E ฮน} [] (hp : ) :
WithSeminorms fun (i : ฮน) => ().sup p
theorem WithSeminorms.congr_equiv {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} {ฮน' : Type u_9} [Nonempty ฮน] [Nonempty ฮน'] [NormedField ๐] [] [Module ๐ E] {p : SeminormFamily ๐ E ฮน} [t : ] (hp : ) (e : ฮน' โ ฮน) :
WithSeminorms (p โ โe)
theorem Seminorm.map_eq_zero_of_norm_zero {๐ : Type u_1} {F : Type u_6} [] [NormedSpace ๐ F] (q : Seminorm ๐ F) (hq : Continuous โq) {x : F} (hx : = 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} [] [NormedSpace ๐ F] (q : Seminorm ๐ F) (hq : Continuous โq) :
โ (C : โ), 0 < C โง โ (x : F), q x โค C *

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} [] [] [Module ๐ E] {p : SeminormFamily ๐ E ฮน} [Nonempty ฮน] [t : ] (hp : ) (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_1} {E : Type u_5} {ฮน : Type u_8} [Nonempty ฮน] [NormedField ๐] [NormedSpace โ ๐] [] [Module ๐ E] [] [IsScalarTower โ ๐ E] [] {p : SeminormFamily ๐ E ฮน} (hp : ) :
theorem NormedSpace.toLocallyConvexSpace' (๐ : Type u_1) {E : Type u_5} [NormedField ๐] [NormedSpace โ ๐] [NormedSpace ๐ E] [] [IsScalarTower โ ๐ 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} [] :

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

Equations
• โฏ = โฏ
def SeminormFamily.comp {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [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
Instances For
theorem SeminormFamily.comp_apply {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [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_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [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_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [] [hฮน : Nonempty ฮน] {q : SeminormFamily ๐โ F ฮน} (hq : ) (f : E โโโ[ฯโโ] F) :
WithSeminorms (q.comp f)
theorem Inducing.withSeminorms {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_5} {F : Type u_6} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] [NormedField ๐โ] [] [Module ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [] [hฮน : Nonempty ฮน] {q : SeminormFamily ๐โ F ฮน} (hq : ) [] {f : E โโโ[ฯโโ] F} (hf : Inducing โf) :
WithSeminorms (q.comp f)
def SeminormFamily.sigma {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] {ฮบ : ฮน โ Type u_10} (p : (i : ฮน) โ SeminormFamily ๐ E (ฮบ i)) :
SeminormFamily ๐ E ((i : ฮน) ร ฮบ i)

(Disjoint) union of seminorm families.

Equations
• = match x with | โจi, kโฉ => p i k
Instances For
theorem withSeminorms_iInf {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐] [] [Module ๐ E] {ฮบ : ฮน โ Type u_10} [Nonempty ((i : ฮน) ร ฮบ i)] [โ (i : ฮน), Nonempty (ฮบ i)] {p : (i : ฮน) โ SeminormFamily ๐ E (ฮบ i)} {t : ฮน โ } [โ (i : ฮน), ] (hp : โ (i : ฮน), WithSeminorms (p i)) :
theorem WithSeminorms.first_countable {๐ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [] [] [Module ๐ E] [Nonempty ฮน] [] {p : SeminormFamily ๐ E ฮน} [] (hp : ) :

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