Theorem ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT

Modification history

2024-11-02 18:11
Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
chore(ContinuousLinearMapWOT): generalize and golf (#17492)
Added ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOTView on Github →