Commit 2023-06-30 16:13 a59175a8

View on Github →

feat: add Metric.Bounded.vadd (#5270) Add Metric.Bounded.smul and Metric.Bounded.vadd, rename the old smul to smul₀.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

deleted theorem Metric.Bounded.smul

added theorem Metric.Bounded.smul₀

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

added theorem Metric.Bounded.smul