Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.bounded.smul

Modification history

2021-12-23 02:02

src/analysis/normed_space/pointwise.lean

feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820) …

Added metric.bounded.smul View on Github →