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

@[reducible, inline]
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
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.

    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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : SeminormFamily ๐•œ E ฮน) [Nonempty ฮน] :
      p.basisSets.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 โˆˆ 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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] (p : SeminormFamily ๐•œ E ฮน) :
          AddGroupFilterBasis.toFilterBasis.filter = โจ… (i : ฮน), Filter.comap (โ‡‘(p i)) (nhds 0)
          theorem SeminormFamily.basisSets_mem_nhds {๐•œ : Type u_10} {E : Type u_11} {ฮน : Type u_12} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] (p : SeminormFamily ๐•œ E ฮน) (hp : โˆ€ (i : ฮน), Continuous โ‡‘(p i)) (U : Set E) (hU : U โˆˆ p.basisSets) :

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

          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.

          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 ๐•œ] [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 : 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 ๐•œ] [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 : 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 ๐•œ] [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 : 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 ๐•œ] [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.

            • 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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] {p : SeminormFamily ๐•œ E ฮน} [topology : TopologicalSpace E] (self : WithSeminorms p) :
              topology = p.moduleFilterBasis.topology
              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 = p.moduleFilterBasis.topology
              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) :
              (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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] [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_1} {E : Type u_5} {ฮน : Type u_8} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] [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_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 : 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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] [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_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, (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 ๐•œ] [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โ‚€ : 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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] [t : TopologicalSpace E] [TopologicalAddGroup E] (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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] [t : TopologicalSpace E] [TopologicalAddGroup E] (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 ๐•œ] [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 : 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} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] {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_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 > 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} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Nonempty ฮน] {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_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 > 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} [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 โ‡‘((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} [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 โ‡‘((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} [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 : 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 ๐•] [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 : 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} [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) :
              [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} [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] [UniformAddGroup 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_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] [UniformAddGroup 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_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) :
              WithSeminorms fun (s : Finset ฮน) => s.sup 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.Iic i).sup 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 : 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 โ„ ๐•œ] [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.

              Equations
              • โ‹ฏ = โ‹ฏ
              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
              • 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 ๐•œ] [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_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) :
                (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 ๐•œ] [AddCommGroup E] [Module ๐•œ E] [NormedField ๐•œโ‚‚] [AddCommGroup F] [Module ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [TopologicalSpace F] [hฮน : Nonempty ฮน] {q : SeminormFamily ๐•œโ‚‚ F ฮน} (hq : WithSeminorms q) (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 ๐•œ] [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 (q.comp 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
                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} (hp : โˆ€ (i : ฮน), WithSeminorms (p i)) :
                  theorem withSeminorms_pi {๐•œ : Type u_1} {ฮน : Type u_8} [NormedField ๐•œ] {ฮบ : ฮน โ†’ Type u_10} {E : ฮน โ†’ Type u_11} [(i : ฮน) โ†’ AddCommGroup (E i)] [(i : ฮน) โ†’ Module ๐•œ (E i)] [(i : ฮน) โ†’ TopologicalSpace (E i)] [Nonempty ((i : ฮน) ร— ฮบ i)] [โˆ€ (i : ฮน), Nonempty (ฮบ 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.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.