Documentation

Mathlib.Topology.Algebra.Module.WeakDual

Weak dual topology #

This file defines the weak topology given two vector spaces E and F over a commutative semiring š•œ and a bilinear form B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ. The weak topology on E is the coarsest topology such that for all y : F every map fun x => B x y is continuous.

In the case that F = E ā†’L[š•œ] š•œ and B being the canonical pairing, we obtain the weak-* topology, WeakDual š•œ E := (E ā†’L[š•œ] š•œ). Interchanging the arguments in the bilinear form yields the weak topology WeakSpace š•œ E := E.

Main definitions #

The main definitions are the types WeakBilin B for the general case and the two special cases WeakDual š•œ E and WeakSpace š•œ E with the respective topology instances on it.

Main results #

We establish that WeakBilin B has the following structure:

We prove the following results characterizing the weak topology:

Notations #

No new notation is introduced.

References #

Tags #

weak-star, weak dual, duality

def WeakBilin {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] :
(E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) ā†’ Type u_5

The space E equipped with the weak topology induced by the bilinear form B.

Equations
Instances For
    instance WeakBilin.instAddCommMonoid {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [a : AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    Equations
    instance WeakBilin.instModule {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [AddCommMonoid E] [m : Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    Module š•œ (WeakBilin B)
    Equations
    instance WeakBilin.instAddCommGroup {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [a : AddCommGroup E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    Equations
    instance WeakBilin.instModule' {š•œ : Type u_2} {š• : Type u_3} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [CommSemiring š•] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] [m : Module š• E] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    Module š• (WeakBilin B)
    Equations
    instance WeakBilin.instIsScalarTower {š•œ : Type u_2} {š• : Type u_3} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [CommSemiring š•] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] [SMul š• š•œ] [Module š• E] [s : IsScalarTower š• š•œ E] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    IsScalarTower š• š•œ (WeakBilin B)
    Equations
    • ā‹Æ = s
    instance WeakBilin.instTopologicalSpace {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    Equations
    theorem WeakBilin.coeFn_continuous {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) :
    Continuous fun (x : WeakBilin B) (y : F) => (B x) y

    The coercion (fun x y => B x y) : E ā†’ (F ā†’ š•œ) is continuous.

    theorem WeakBilin.eval_continuous {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) (y : F) :
    Continuous fun (x : WeakBilin B) => (B x) y
    theorem WeakBilin.continuous_of_continuous_eval {Ī± : Type u_1} {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) [TopologicalSpace Ī±] {g : Ī± ā†’ WeakBilin B} (h : āˆ€ (y : F), Continuous fun (a : Ī±) => (B (g a)) y) :
    theorem WeakBilin.embedding {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] {B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ} (hB : Function.Injective ā‡‘B) :
    Embedding fun (x : WeakBilin B) (y : F) => (B x) y

    The coercion (fun x y => B x y) : E ā†’ (F ā†’ š•œ) is an embedding.

    theorem WeakBilin.tendsto_iff_forall_eval_tendsto {Ī± : Type u_1} {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) {l : Filter Ī±} {f : Ī± ā†’ WeakBilin B} {x : WeakBilin B} (hB : Function.Injective ā‡‘B) :
    Filter.Tendsto f l (nhds x) ā†” āˆ€ (y : F), Filter.Tendsto (fun (i : Ī±) => (B (f i)) y) l (nhds ((B x) y))
    instance WeakBilin.instContinuousAdd {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) [ContinuousAdd š•œ] :

    Addition in WeakBilin B is continuous.

    Equations
    • ā‹Æ = ā‹Æ
    instance WeakBilin.instContinuousSMul {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommSemiring š•œ] [AddCommMonoid E] [Module š•œ E] [AddCommMonoid F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) [ContinuousSMul š•œ š•œ] :

    Scalar multiplication by š•œ on WeakBilin B is continuous.

    Equations
    • ā‹Æ = ā‹Æ
    instance WeakBilin.instTopologicalAddGroup {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace š•œ] [CommRing š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] (B : E ā†’ā‚—[š•œ] F ā†’ā‚—[š•œ] š•œ) [ContinuousAdd š•œ] :

    WeakBilin B is a TopologicalAddGroup, meaning that addition and negation are continuous.

    Equations
    • ā‹Æ = ā‹Æ
    def topDualPairing (š•œ : Type u_8) (E : Type u_9) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] [ContinuousConstSMul š•œ š•œ] :
    (E ā†’L[š•œ] š•œ) ā†’ā‚—[š•œ] E ā†’ā‚—[š•œ] š•œ

    The canonical pairing of a vector space and its topological dual.

    Equations
    Instances For
      theorem topDualPairing_apply {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (v : E ā†’L[š•œ] š•œ) (x : E) :
      ((topDualPairing š•œ E) v) x = v x
      def WeakDual (š•œ : Type u_8) (E : Type u_9) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
      Type (max u_8 u_9)

      The weak star topology is the topology coarsest topology on E ā†’L[š•œ] š•œ such that all functionals fun v => v x are continuous.

      Equations
      Instances For
        instance WeakDual.instAddCommMonoid {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        AddCommMonoid (WeakDual š•œ E)
        Equations
        instance WeakDual.instModule {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        Module š•œ (WeakDual š•œ E)
        Equations
        instance WeakDual.instTopologicalSpace {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        Equations
        instance WeakDual.instContinuousAdd {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        ContinuousAdd (WeakDual š•œ E)
        Equations
        • ā‹Æ = ā‹Æ
        instance WeakDual.instInhabited {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        Inhabited (WeakDual š•œ E)
        Equations
        • WeakDual.instInhabited = ContinuousLinearMap.inhabited
        instance WeakDual.instFunLike {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        FunLike (WeakDual š•œ E) E š•œ
        Equations
        • WeakDual.instFunLike = ContinuousLinearMap.funLike
        instance WeakDual.instContinuousLinearMapClass {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        ContinuousLinearMapClass (WeakDual š•œ E) š•œ E š•œ
        Equations
        • ā‹Æ = ā‹Æ
        instance WeakDual.instCoeFunWeakDualForAll {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        CoeFun (WeakDual š•œ E) fun (x : WeakDual š•œ E) => E ā†’ š•œ

        Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

        Equations
        • WeakDual.instCoeFunWeakDualForAll = DFunLike.hasCoeToFun
        instance WeakDual.instMulAction {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M š•œ] [SMulCommClass š•œ M š•œ] [ContinuousConstSMul M š•œ] :
        MulAction M (WeakDual š•œ E)

        If a monoid M distributively continuously acts on š•œ and this action commutes with multiplication on š•œ, then it acts on WeakDual š•œ E.

        Equations
        instance WeakDual.instDistribMulAction {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M š•œ] [SMulCommClass š•œ M š•œ] [ContinuousConstSMul M š•œ] :
        DistribMulAction M (WeakDual š•œ E)

        If a monoid M distributively continuously acts on š•œ and this action commutes with multiplication on š•œ, then it acts distributively on WeakDual š•œ E.

        Equations
        instance WeakDual.instModule' {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (R : Type u_8) [Semiring R] [Module R š•œ] [SMulCommClass š•œ R š•œ] [ContinuousConstSMul R š•œ] :
        Module R (WeakDual š•œ E)

        If š•œ is a topological module over a semiring R and scalar multiplication commutes with the multiplication on š•œ, then WeakDual š•œ E is a module over R.

        Equations
        instance WeakDual.instContinuousConstSMul {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M š•œ] [SMulCommClass š•œ M š•œ] [ContinuousConstSMul M š•œ] :
        Equations
        • ā‹Æ = ā‹Æ
        instance WeakDual.instContinuousSMul {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M š•œ] [SMulCommClass š•œ M š•œ] [TopologicalSpace M] [ContinuousSMul M š•œ] :
        ContinuousSMul M (WeakDual š•œ E)

        If a monoid M distributively continuously acts on š•œ and this action commutes with multiplication on š•œ, then it continuously acts on WeakDual š•œ E.

        Equations
        • ā‹Æ = ā‹Æ
        theorem WeakDual.coeFn_continuous {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        Continuous fun (x : WeakDual š•œ E) (y : E) => x y
        theorem WeakDual.eval_continuous {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (y : E) :
        Continuous fun (x : WeakDual š•œ E) => x y
        theorem WeakDual.continuous_of_continuous_eval {Ī± : Type u_1} {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] [TopologicalSpace Ī±] {g : Ī± ā†’ WeakDual š•œ E} (h : āˆ€ (y : E), Continuous fun (a : Ī±) => (g a) y) :
        instance WeakDual.instT2Space {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] [T2Space š•œ] :
        T2Space (WeakDual š•œ E)
        Equations
        • ā‹Æ = ā‹Æ
        def WeakSpace (š•œ : Type u_8) (E : Type u_9) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
        Type u_9

        The weak topology is the topology coarsest topology on E such that all functionals fun x => v x are continuous.

        Equations
        Instances For
          instance WeakSpace.instAddCommMonoid {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
          Equations
          instance WeakSpace.instModule {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
          Module š•œ (WeakSpace š•œ E)
          Equations
          instance WeakSpace.instTopologicalSpace {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
          Equations
          instance WeakSpace.instContinuousAdd {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
          Equations
          • ā‹Æ = ā‹Æ
          def WeakSpace.map {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] [AddCommMonoid F] [Module š•œ F] [TopologicalSpace F] (f : E ā†’L[š•œ] F) :
          WeakSpace š•œ E ā†’L[š•œ] WeakSpace š•œ F

          A continuous linear map from E to F is still continuous when E and F are equipped with their weak topologies.

          Equations
          Instances For
            theorem WeakSpace.map_apply {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] [AddCommMonoid F] [Module š•œ F] [TopologicalSpace F] (f : E ā†’L[š•œ] F) (x : E) :
            (WeakSpace.map f) x = f x
            @[simp]
            theorem WeakSpace.coe_map {š•œ : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] [AddCommMonoid F] [Module š•œ F] [TopologicalSpace F] (f : E ā†’L[š•œ] F) :
            ā‡‘(WeakSpace.map f) = ā‡‘f
            def toWeakSpace (š•œ : Type u_2) (E : Type u_5) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
            E ā‰ƒā‚—[š•œ] WeakSpace š•œ E

            There is a canonical map E ā†’ WeakSpace š•œ E (the "identity" mapping). It is a linear equivalence.

            Equations
            Instances For
              def continuousLinearMapToWeakSpace (š•œ : Type u_2) (E : Type u_5) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
              E ā†’L[š•œ] WeakSpace š•œ E

              For a topological vector space E, "identity mapping" E ā†’ WeakSpace š•œ E is continuous. This definition implements it as a continuous linear map.

              Equations
              Instances For
                @[simp]
                theorem continuousLinearMapToWeakSpace_eq_toWeakSpace (š•œ : Type u_2) (E : Type u_5) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (x : E) :
                (continuousLinearMapToWeakSpace š•œ E) x = (toWeakSpace š•œ E) x
                theorem continuousLinearMapToWeakSpace_bijective {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :
                theorem isOpenMap_toWeakSpace_symm {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] :

                The canonical map from WeakSpace š•œ E to E is an open map.

                theorem WeakSpace.isOpen_of_isOpen {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] (V : Set E) (hV : IsOpen (ā‡‘(continuousLinearMapToWeakSpace š•œ E) '' V)) :

                A set in E which is open in the weak topology is open.

                theorem tendsto_iff_forall_eval_tendsto_topDualPairing {Ī± : Type u_1} {š•œ : Type u_2} {E : Type u_5} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [AddCommMonoid E] [Module š•œ E] [TopologicalSpace E] {l : Filter Ī±} {f : Ī± ā†’ WeakDual š•œ E} {x : WeakDual š•œ E} :
                Filter.Tendsto f l (nhds x) ā†” āˆ€ (y : E), Filter.Tendsto (fun (i : Ī±) => ((topDualPairing š•œ E) (f i)) y) l (nhds (((topDualPairing š•œ E) x) y))