Theorem ContinuousLinearMapWOT.isInducing_inducingFn

Modification history

2025-10-18 15:19
Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
feat(Analysis): semilinearize `ContinuousLinearMapWOT` (#30597)
Modified ContinuousLinearMapWOT.isInducing_inducingFnView on Github →
2024-11-02 18:11
Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
chore(ContinuousLinearMapWOT): generalize and golf (#17492)
Added ContinuousLinearMapWOT.isInducing_inducingFnView on Github →