Commit 2025-10-18 15:19 ded3210a

View on Github →

feat(Analysis): semilinearize ContinuousLinearMapWOT (#30597)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

modified theorem ContinuousLinearMap.toWOT_apply

modified def ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM

modified theorem ContinuousLinearMapWOT.add_apply

modified theorem ContinuousLinearMapWOT.continuous_dual_apply

modified theorem ContinuousLinearMapWOT.continuous_inducingFn

modified theorem ContinuousLinearMapWOT.continuous_of_dual_apply_continuous

modified theorem ContinuousLinearMapWOT.ext

modified theorem ContinuousLinearMapWOT.ext_dual

modified theorem ContinuousLinearMapWOT.ext_iff

modified theorem ContinuousLinearMapWOT.hasBasis_seminorms

modified def ContinuousLinearMapWOT.inducingFn

modified theorem ContinuousLinearMapWOT.inducingFn_apply

modified theorem ContinuousLinearMapWOT.isEmbedding_inducingFn

modified theorem ContinuousLinearMapWOT.isInducing_inducingFn

modified theorem ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds

modified theorem ContinuousLinearMapWOT.neg_apply

modified def ContinuousLinearMapWOT.seminorm

modified def ContinuousLinearMapWOT.seminormFamily

modified theorem ContinuousLinearMapWOT.smul_apply

modified theorem ContinuousLinearMapWOT.sub_apply

modified theorem ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto

modified theorem ContinuousLinearMapWOT.withSeminorms

modified theorem ContinuousLinearMapWOT.zero_apply

modified def ContinuousLinearMapWOT