Theorem Continuous.continuousLinearMapCoprod

Modification history

2025-06-23 08:19
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
feat(Analysis/Normed/Operator): continuity of forming ContinuousLinearMap coproducts pointwise (#26273) …
Added Continuous.continuousLinearMapCoprodView on Github →