Closures of convex sets in locally convex spaces

This file contains the standard result that if E is a vector space with two locally convex topologies, then the closure of a convex set is the same in either topology, provided they have the same collection of continuous linear functionals. In particular, the weak closure of a convex set in a locally convex space coincides with the closure in the original topology. Of course, we phrase this in terms of linear maps between locally convex spaces, rather than creating two separate topologies on the same space.

theorem Convex.toWeakSpace_closure (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {s : Set E} (hs : Convex ℝ s) : ⇑(toWeakSpace 𝕜 E) '' closure s = closure (⇑(toWeakSpace 𝕜 E) '' s)

If E is a locally convex space over 𝕜 (with RCLike 𝕜), and s : Set E is ℝ-convex, then the closure of s and the weak closure of s coincide. More precisely, the topological closure commutes with toWeakSpace 𝕜 E.

This holds more generally for any linear equivalence e : E ≃ₗ[𝕜] F between locally convex spaces such that precomposition with e and e.symm preserves continuity of linear functionals. See LinearEquiv.image_closure_of_convex.

theorem LinearMap.image_closure_of_convex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [LocallyConvexSpace ℝ F] {s : Set E} (hs : Convex ℝ s) (e : E →ₗ[𝕜] F) (he : ∀ (f : F →L[𝕜] 𝕜), Continuous ⇑(e.dualMap ↑f)) : ⇑e '' closure s ⊆ closure (⇑e '' s)

If e : E →ₗ[𝕜] F is a linear map between locally convex spaces, and f ∘ e is continuous for every continuous linear functional f : F →L[𝕜] 𝕜, then e commutes with the closure on convex sets.

theorem LinearEquiv.image_closure_of_convex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [LocallyConvexSpace ℝ F] {s : Set E} (hs : Convex ℝ s) (e : E ≃ₗ[𝕜] F) (he₁ : ∀ (f : F →L[𝕜] 𝕜), Continuous ⇑(e.dualMap ↑f)) (he₂ : ∀ (f : E →L[𝕜] 𝕜), Continuous ⇑(e.symm.dualMap ↑f)) : ⇑e '' closure s = closure (⇑e '' s)

If e is a linear isomorphism between two locally convex spaces, and e induces (via precomposition) an isomorphism between their continuous duals, then e commutes with the closure on convex sets.

The hypotheses hold automatically for e := toWeakSpace 𝕜 E, see Convex.toWeakSpace_closure.

theorem LinearEquiv.image_closure_of_convex' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [LocallyConvexSpace ℝ F] {s : Set E} (hs : Convex ℝ s) (e : E ≃ₗ[𝕜] F) (e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)) (he : ∀ (f : F →L[𝕜] 𝕜), ↑(e_dual f) = e.dualMap ↑f) : ⇑e '' closure s = closure (⇑e '' s)

If e is a linear isomorphism between two locally convex spaces, and e induces (via precomposition) an isomorphism between their continuous duals, then e commutes with the closure on convex sets.

The hypotheses hold automatically for e := toWeakSpace 𝕜 E, see Convex.toWeakSpace_closure.