Lean: "weak-topology continuous ⇒ in the family" when the family is itself linear

To show a functional continuous for the topology ⨅ T, induced (G T) is some G T (e.g. σ-weakly continuous functionals on B(H) are tr(· T)), bundle the family as a linear map G : V →ₗ[𝕜] (E →ₗ[𝕜] 𝕜) (a .flip of (ContinuousLinearMap.coeLM 𝕜).comp e.toLinearMap works) and then rw [← LinearMap.mem_span_iff_continuous, ← LinearMap.coe_range, Submodule.span_eq]: the span of the range of a linear map is the range, so no finsupp bookkeeping is needed. Notation gotcha: Continuous[t₁, t₂] f is scoped and needs open Topology. Without it you get the misleading parse error "unexpected token ','; expected ':', ']'". A def of type TopologicalSpace X should get @[instance_reducible] to silence the class-def reducibility warning.