Commit 2026-01-07 14:55 a9b1c38b

View on Github →

chore: more fun_prop attributes and lemmas (#33671)

Estimated changes

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

added theorem ContinuousAt.clm_comp

added theorem ContinuousAt.continuousLinearMapCoprod

added theorem ContinuousWithinAt.clm_comp

added theorem ContinuousWithinAt.continuousLinearMapCoprod

Modified Mathlib/Topology/Algebra/Monoid/Defs.lean

Modified Mathlib/Topology/ContinuousOn.lean

modified theorem ContinuousAt.comp_continuousWithinAt