English
Let e: E →ₗ[𝕜] F be a linear map between locally convex spaces. If for every continuous functional f on F, the composed map e.dualMap f is continuous, then e carries the closure of a convex set to the closure of its image.
Русский
Пусть e: E →ₗ[𝕜] F — линейное отображение между локально выпуклыми пространствами. Если для каждого непрерывного функционала f на F композиция e.dualMap f непрерывна, то e переносит замыкание выпуклого множества в замыкание его образа.
LaTeX
$$theorem image_closure_of_convex {s : Set E} (hs : Convex ℝ s) (e : E →ₗ[𝕜] F) (he : ∀ f : StrongDual 𝕜 F, Continuous (e.dualMap f)) : e '' (closure s) ⊆ closure (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)
(he₁ : ∀ f : StrongDual 𝕜 F, Continuous (e.dualMap f)) (he₂ : ∀ f : StrongDual 𝕜 E, Continuous (e.symm.dualMap f)) :
e '' (closure s) = closure (e '' s) :=
by
refine le_antisymm ((e : E →ₗ[𝕜] F).image_closure_of_convex hs he₁) ?_
simp only [Set.le_eq_subset, ← Set.image_subset_image_iff e.symm.injective]
simpa [Set.image_image] using (e.symm : F →ₗ[𝕜] E).image_closure_of_convex (hs.linear_image (e : E →ₗ[𝕜] F)) he₂
