LeanPool.SardMoreira.NormedSpace

theorem NNReal.norm_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : NNReal) (x : E) : ‖a • x‖ = ↑a * ‖x‖

theorem NNReal.nnnorm_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : NNReal) (x : E) : ‖a • x‖₊ = a * ‖x‖₊

theorem NNReal.enorm_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : NNReal) (x : E) : ‖a • x‖ₑ = ↑a * ‖x‖ₑ

theorem NNReal.dist_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : NNReal) (x y : E) : dist (a • x) (a • y) = ↑a * dist x y

theorem NNReal.nndist_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : NNReal) (x y : E) : nndist (a • x) (a • y) = a * nndist x y

theorem NNReal.edist_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : NNReal) (x y : E) : edist (a • x) (a • y) = ↑a * edist x y