Commit 2026-06-10 22:10 55a83a22

View on Github →

feat: star structures on ContinuousLinearMapWOT (#39163) In particular, with these instances it makes sense to consider the StarSubalgebra.topologicalClosure of some S : StarSubalgebra 𝕜 (F →WOT[𝕜] F).

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean

added theorem ContinuousLinearMapWOT.continuousAt_iff

added theorem ContinuousLinearMapWOT.continuousOn_iff

added theorem ContinuousLinearMapWOT.continuousWithinAt_iff

added theorem ContinuousLinearMapWOT.continuous_iff

modified theorem ContinuousLinearMapWOT.le_nhds_iff_forall_inner_apply_le_nhds

added theorem ContinuousLinearMapWOT.star_apply

modified theorem ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto