Theorems · Theorem · functional analysis

Convex.toWeakSpace_closure

∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Module ℝ E]
  [IsScalarTower ℝ 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] {s : Set E}, 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.

Defined in

Mathlib.Analysis.LocallyConvex.WeakSpace

Cited by

2 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeAddCommGroupModuleModuleIsScalarTowerTopologicalSpaceIsTopologicalAddGroupContinuousSMulLocallyConvexSpace