Theorems · Theorem · functional analysis

IsOpen.smul_sphere

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  r ≠ 0 → ∀ {U : Set ℝ} {V : Set ↑(Metric.sphere 0 r)}, IsOpen U → 0 ∉ U → IsOpen V → IsOpen (U • Subtype.val '' V)

If U ∌ 0 is an open set on the real line and V is an open set on a sphere of nonzero radius, then their pointwise scalar product is an open set.

Defined in

Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace