Documentation

Mathlib.Analysis.LocallyConvex.WithSeminorms

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 LinearMap.continuous_of_locally_bounded this gives general criterion for continuity.

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.

Instances For
    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.

    Instances For
      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} :
      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) :
      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) :
      theorem SeminormFamily.basisSets_nonempty {๐•œ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : SeminormFamily ๐•œ E ฮน) [Nonempty ฮน] :
      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) :
      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) :
      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) :
      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) :
      def SeminormFamily.addGroupFilterBasis {๐•œ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : SeminormFamily ๐•œ E ฮน) [Nonempty ฮน] :

      The addGroupFilterBasis induced by the filter basis Seminorm.basisSets.

      Instances For
        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.

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

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

          Instances For
            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 ฮน') :
            structure WithSeminorms {๐•œ : Type u_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] (p : SeminormFamily ๐•œ E ฮน) [topology : TopologicalSpace E] :

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

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

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

              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) :
              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) :
              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) :
              theorem NormedSpace.toLocallyConvexSpace' (๐•œ : Type u_1) {E : Type u_5} [NormedField ๐•œ] [NormedSpace โ„ ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] [Module โ„ E] [IsScalarTower โ„ ๐•œ E] :

              Not an instance since ๐•œ can't be inferred. See NormedSpace.toLocallyConvexSpace for a slightly weaker instance version.

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

              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.

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

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

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