theorem continuousAffineMap_continuous_toWeakSpace {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H →ᴬ[ℝ] K) : Continuous fun (x : WeakSpace ℝ H) => (toWeakSpace ℝ K) (T ((toWeakSpace ℝ H).symm x))

Lemma 2.41: a continuous affine map between real normed spaces is continuous from the weak topology on the domain to the weak topology on the codomain.

theorem continuousAffineMap_tendsto_toWeakSpace {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {A : Type w} [Preorder A] [IsDirectedOrder A] (T : H →ᴬ[ℝ] K) {ξ : A → H} {x : H} (hξ : Filter.Tendsto (fun (a : A) => (toWeakSpace ℝ H) (ξ a)) Filter.atTop (nhds ((toWeakSpace ℝ H) x))) : Filter.Tendsto (fun (a : A) => (toWeakSpace ℝ K) (T (ξ a))) Filter.atTop (nhds ((toWeakSpace ℝ K) (T x)))

A weakly convergent directed net remains weakly convergent after application of a continuous affine map.