English
The weak space map commutes with taking closed convex hulls: the image of the closed convex hull equals the closed convex hull of the image.
Русский
Отображение в слабое пространство commute с операцией замыкания выпуклого множества: образ замкнутой выпуклой оболочки равен замыканию образа.
LaTeX
$$toWeakSpace_closedConvexHull_eq {s : Set E} : (toWeakSpace 𝕜 E) '' (closedConvexHull 𝕜 s) = closedConvexHull 𝕜 (toWeakSpace 𝕜 E '' s)$$
Lean4
/-- 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 image_closure_of_convex' {s : Set E} (hs : Convex ℝ s) (e : E ≃ₗ[𝕜] F)
(e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E) (he : ∀ f : StrongDual 𝕜 F, (e_dual f : E →ₗ[𝕜] 𝕜) = e.dualMap f) :
e '' (closure s) = closure (e '' s) :=
by
have he' (f : StrongDual 𝕜 E) : (e_dual.symm f : F →ₗ[𝕜] 𝕜) = e.symm.dualMap f :=
by
simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢
have (g : StrongDual 𝕜 E) : ⇑g = e_dual.symm g ∘ e :=
by
have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
simpa
ext x
conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]
simp
refine e.image_closure_of_convex hs ?_ ?_
· simpa [← he] using fun f ↦ map_continuous (e_dual f)
· simpa [← he'] using fun f ↦ map_continuous (e_dual.symm f)
