English
Reiterates the uniform additive group structure on the WOT space.
Русский
Повторно утверждается униформная группа по сложению для WOT пространства.
LaTeX
$$IsUniformAddGroup (ContinuousLinearMapWOT 𝕜 E F)$$
Lean4
/-- If `e : E →ₗ[𝕜] F` is a linear map between locally convex spaces, and `f ∘ e` is continuous
for every continuous linear functional `f : StrongDual 𝕜 F`, then `e` commutes with the closure on
convex sets. -/
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) :=
by
suffices he' : Continuous (toWeakSpace 𝕜 F <| e <| (toWeakSpace 𝕜 E).symm ·)
by
have h_convex : Convex ℝ (e '' s) := hs.linear_image (F := F) e
rw [← Set.image_subset_image_iff (toWeakSpace 𝕜 F).injective, h_convex.toWeakSpace_closure 𝕜]
simpa only [Set.image_image, ← hs.toWeakSpace_closure 𝕜, LinearEquiv.symm_apply_apply] using
he'.continuousOn.image_closure (s := toWeakSpace 𝕜 E '' s)
exact
WeakBilin.continuous_of_continuous_eval _ fun f ↦
WeakBilin.eval_continuous _ { toLinearMap := e.dualMap f : StrongDual 𝕜 E }
