Def ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM

Modification history

2025-10-18 15:19

Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

feat(Analysis): semilinearize `ContinuousLinearMapWOT` (#30597)

Modified ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM View on Github →

2024-11-02 18:11

Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

chore(ContinuousLinearMapWOT): generalize and golf (#17492)

Added ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM View on Github →