Commit 2024-11-02 18:11 2fc69c7f

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean

Renamed Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean to Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

deleted theorem ContinuousLinearMap.continuous_toWOT

modified def ContinuousLinearMap.toWOT

deleted def ContinuousLinearMap.toWOTCLM

added theorem ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT

added def ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM

modified theorem ContinuousLinearMapWOT.ext_dual

modified theorem ContinuousLinearMapWOT.hasBasis_seminorms

added theorem ContinuousLinearMapWOT.inducingFn_apply

modified theorem ContinuousLinearMapWOT.isEmbedding_inducingFn

added theorem ContinuousLinearMapWOT.isInducing_inducingFn