Theorem ContinuousLinearMapWOT.inducingFn_apply

Modification history

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