English
For a convex set s, the weak closure of s after applying toWeakSpace coincides with the closure of the image of s.
Русский
Для выпуклого множества s слабая его замкнутая оболочка после применения toWeakSpace совпадает с замыканием образа s.
LaTeX
$$toWeakSpace_closure {s : Set E} (hs : Convex ℝ s) : (toWeakSpace 𝕜 E) '' (closure s) = closure (toWeakSpace 𝕜 E '' s)$$
Lean4
/-- 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 toWeakSpace_closure {s : Set E} (hs : Convex ℝ s) :
(toWeakSpace 𝕜 E) '' (closure s) = closure (toWeakSpace 𝕜 E '' s) :=
by
refine
le_antisymm (map_continuous <| toWeakSpaceCLM 𝕜 E).continuousOn.image_closure
(Set.compl_subset_compl.mp fun x hx ↦ ?_)
obtain ⟨x, -, rfl⟩ := (toWeakSpace 𝕜 E).toEquiv.image_compl (closure s) |>.symm.subset hx
have : ContinuousSMul ℝ E := IsScalarTower.continuousSMul 𝕜
obtain ⟨f, u, hus, hux⟩ :=
RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs.closure isClosed_closure (by simpa using hx)
let f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
{ toLinearMap := (f : E →ₗ[𝕜] 𝕜).comp ((toWeakSpace 𝕜 E).symm : WeakSpace 𝕜 E →ₗ[𝕜] E)
cont := WeakBilin.eval_continuous (topDualPairing 𝕜 E).flip _ }
have hux' : u < RCLike.reCLM.comp (f'.restrictScalars ℝ) (toWeakSpace 𝕜 E x) := by simpa [f']
have hus' : closure (toWeakSpace 𝕜 E '' s) ⊆ {y | RCLike.reCLM.comp (f'.restrictScalars ℝ) y ≤ u} :=
by
refine closure_minimal ?_ <| isClosed_le (by fun_prop) (by fun_prop)
rintro - ⟨y, hy, rfl⟩
simpa [f'] using (hus y <| subset_closure hy).le
exact (hux'.not_ge <| hus' ·)
