Theorem ContinuousLinearMapWOT.isInducing_inducingFn

Modification history

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