Theorems · Theorem · functional analysis

smul_sphere

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [NormedSpace ℝ E] [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ},
  0 ≤ r → c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)

Defined in

Mathlib.Analysis.Normed.Module.Ball.Pointwise

Cited by

1 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldNormedAddCommGroupNormedSpaceNormedSpaceNontrivial