Theorem ContinuousWithinAt.continuousLinearMapCoprod

Modification history

2026-01-07 14:55
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
chore: more `fun_prop` attributes and lemmas (#33671)
Added ContinuousWithinAt.continuousLinearMapCoprodView on Github →