Documentation

Mathlib.Topology.Algebra.Module.WeakDual

Weak dual topology #

We continue in the setting of Mathlib/Topology/Algebra/Module/WeakBilin.lean, which 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 this file, we consider two special cases. 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 WeakDual 𝕜 E and WeakSpace 𝕜 E, with the respective topology instances on it.

WeakDual 𝕜 E is a type synonym for Dual 𝕜 E (when the latter is defined): both are equal to the type E →L[𝕜] 𝕜 of continuous linear maps from a module E over 𝕜 to the ring 𝕜.
The instance WeakDual.instTopologicalSpace is the weak-* topology on WeakDual 𝕜 E, i.e., the coarsest topology making the evaluation maps at all z : E continuous.
WeakSpace 𝕜 E is a type synonym for E (when the latter is defined).
The instance WeakSpace.instTopologicalSpace is the weak topology on E, i.e., the coarsest topology such that all v : dual 𝕜 E remain continuous.

References #

H. H. Schaefer, Topological Vector Spaces

Tags #

weak-star, weak dual, duality

def WeakDual (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

Type (max u_6 u_7)

The weak star topology is the topology coarsest topology on E →L[𝕜] 𝕜 such that all functionals fun v => v x are continuous.

Equations

WeakDual 𝕜 E = WeakBilin (topDualPairing 𝕜 E)

Instances For

@[implicit_reducible]

noncomputable instance instAddCommMonoidWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

AddCommMonoid (WeakDual 𝕜 E)

Equations

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

@[implicit_reducible]

noncomputable instance instModuleWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

Module 𝕜 (WeakDual 𝕜 E)

Equations

instModuleWeakDual 𝕜 E = { smul := instModuleWeakDual._aux_1 𝕜 E, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

noncomputable instance instTopologicalSpaceWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

TopologicalSpace (WeakDual 𝕜 E)

Equations

instTopologicalSpaceWeakDual 𝕜 E = { IsOpen := instTopologicalSpaceWeakDual._aux_1 𝕜 E, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

@[implicit_reducible]

noncomputable instance instContinuousAddWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

ContinuousAdd (WeakDual 𝕜 E)

Equations

⋯ = ⋯

@[implicit_reducible]

noncomputable instance instInhabitedWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

Inhabited (WeakDual 𝕜 E)

Equations

instInhabitedWeakDual 𝕜 E = { default := instInhabitedWeakDual._aux_1 𝕜 E }

@[implicit_reducible]

noncomputable instance instFunLikeWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

FunLike (WeakDual 𝕜 E) E 𝕜

Equations

instFunLikeWeakDual 𝕜 E = { coe := instFunLikeWeakDual._aux_1 𝕜 E, coe_injective' := ⋯ }

@[implicit_reducible]

noncomputable instance instContinuousLinearMapClassWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜

Equations

⋯ = ⋯

def StrongDual.toWeakDual {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

StrongDual 𝕜 E ≃ₗ[𝕜] WeakDual 𝕜 E

For vector spaces E, there is a canonical map StrongDual 𝕜 E → WeakDual 𝕜 E (the "identity" mapping). It is a linear equivalence.

Equations

StrongDual.toWeakDual = LinearEquiv.refl 𝕜 (StrongDual 𝕜 E)

Instances For

theorem StrongDual.coe_toWeakDual {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x' : StrongDual 𝕜 E) :

⇑(toWeakDual x') = ⇑x'

@[simp]

theorem StrongDual.toWeakDual_apply {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x' : StrongDual 𝕜 E) (y : E) :

(toWeakDual x') y = x' y

theorem StrongDual.toWeakDual_inj {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x' y' : StrongDual 𝕜 E) :

toWeakDual x' = toWeakDual y' ↔ x' = y'

noncomputable def WeakDual.toStrongDual {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

WeakDual 𝕜 E ≃ₗ[𝕜] StrongDual 𝕜 E

For vector spaces E, there is a canonical map WeakDual 𝕜 E → StrongDual 𝕜 E (the "identity" mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear equivalence StrongDual.toWeakDual in the other direction.

Equations

WeakDual.toStrongDual = StrongDual.toWeakDual.symm

Instances For

@[simp]

theorem WeakDual.toStrongDual_apply {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x : WeakDual 𝕜 E) (y : E) :

(toStrongDual x) y = x y

theorem WeakDual.coe_toStrongDual {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x' : WeakDual 𝕜 E) :

⇑(toStrongDual x') = ⇑x'

theorem WeakDual.toStrongDual_inj {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x' y' : WeakDual 𝕜 E) :

toStrongDual x' = toStrongDual y' ↔ x' = y'

@[implicit_reducible]

instance WeakDual.instMulAction {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [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

WeakDual.instMulAction M = { smul := WeakDual.instMulAction._aux_1 M, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance WeakDual.instDistribMulAction {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [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

WeakDual.instDistribMulAction M = { toMulAction := WeakDual.instMulAction M, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance WeakDual.instModule' {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (R : Type u_6) [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

WeakDual.instModule' R = { toDistribMulAction := WeakDual.instDistribMulAction R, add_smul := ⋯, zero_smul := ⋯ }

instance WeakDual.instContinuousConstSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :

ContinuousConstSMul M (WeakDual 𝕜 E)

instance WeakDual.instContinuousSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [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.

theorem WeakDual.coeFn_continuous {𝕜 : Type u_2} {E : Type u_4} [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_4} [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_4} [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_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [T2Space 𝕜] :

T2Space (WeakDual 𝕜 E)

@[implicit_reducible]

noncomputable instance WeakDual.instAddCommGroup {𝕜 : Type u_2} {E : Type u_4} [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] :

AddCommGroup (WeakDual 𝕜 E)

Equations

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

instance WeakDual.instIsTopologicalAddGroup {𝕜 : Type u_2} {E : Type u_4} [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] :

IsTopologicalAddGroup (WeakDual 𝕜 E)

def WeakSpace (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

Type u_7

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

Equations

WeakSpace 𝕜 E = WeakBilin (topDualPairing 𝕜 E).flip

Instances For

@[implicit_reducible]

noncomputable instance instAddCommMonoidWeakSpace (𝕜 : Type u_2) (E : Type u_1) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

AddCommMonoid (WeakSpace 𝕜 E)

Equations

instAddCommMonoidWeakSpace 𝕜 E = instAddCommMonoidWeakSpace._aux_1 𝕜 E

@[implicit_reducible]

noncomputable instance instModuleWeakSpace (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

Module 𝕜 (WeakSpace 𝕜 E)

Equations

instModuleWeakSpace 𝕜 E = instModuleWeakSpace._aux_1 𝕜 E

@[implicit_reducible]

noncomputable instance instTopologicalSpaceWeakSpace (𝕜 : Type u_2) (E : Type u_1) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

TopologicalSpace (WeakSpace 𝕜 E)

Equations

instTopologicalSpaceWeakSpace 𝕜 E = { IsOpen := instTopologicalSpaceWeakSpace._aux_1 𝕜 E, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

@[implicit_reducible]

noncomputable instance instContinuousAddWeakSpace (𝕜 : Type u_2) (E : Type u_1) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

ContinuousAdd (WeakSpace 𝕜 E)

Equations

⋯ = ⋯

@[implicit_reducible]

instance WeakSpace.instModule' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [CommSemiring 𝕝] [Module 𝕝 E] :

Module 𝕝 (WeakSpace 𝕜 E)

Equations

WeakSpace.instModule' = WeakSpace.instModule'._aux_1

instance WeakSpace.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :

IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E)

instance WeakSpace.instContinuousSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 𝕜] :

ContinuousSMul 𝕜 (WeakSpace 𝕜 E)

def WeakSpace.map {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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

WeakSpace.map f = { toLinearMap := ↑f, cont := ⋯ }

Instances For

theorem WeakSpace.map_apply {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) (x : E) :

(map f) x = f x

@[simp]

theorem WeakSpace.coe_map {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) :

⇑(map f) = ⇑f

def toWeakSpace (𝕜 : Type u_2) (E : Type u_4) [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

toWeakSpace 𝕜 E = LinearEquiv.refl 𝕜 E

Instances For

def toWeakSpaceCLM (𝕜 : Type u_2) (E : Type u_4) [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

toWeakSpaceCLM 𝕜 E = { toLinearMap := ↑(toWeakSpace 𝕜 E), cont := ⋯ }

Instances For

@[simp]

theorem toWeakSpaceCLM_eq_toWeakSpace (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x : E) :

(toWeakSpaceCLM 𝕜 E) x = (toWeakSpace 𝕜 E) x

theorem toWeakSpaceCLM_bijective {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

Function.Bijective ⇑(toWeakSpaceCLM 𝕜 E)

theorem isOpenMap_toWeakSpace_symm {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

IsOpenMap ⇑(toWeakSpace 𝕜 E).symm

The canonical map from WeakSpace 𝕜 E to E is an open map.

theorem WeakSpace.isOpen_of_isOpen {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (V : Set E) (hV : IsOpen (⇑(toWeakSpaceCLM 𝕜 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_4} [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))

@[implicit_reducible]

instance WeakSpace.instAddCommGroup {𝕜 : Type u_2} {E : Type u_4} [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] :

AddCommGroup (WeakSpace 𝕜 E)

Equations

WeakSpace.instAddCommGroup = WeakSpace.instAddCommGroup._aux_1

instance WeakSpace.instIsTopologicalAddGroup {𝕜 : Type u_2} {E : Type u_4} [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] :

IsTopologicalAddGroup (WeakSpace 𝕜 E)