Theorems · Theorem · general topology

sphere_pi

∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b)
  {r : ℝ},
  0 < r ∨ Nonempty β → Metric.sphere x r = (⋃ i, Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r

A sphere in a product space is a union of spheres on each component restricted to the closed ball.

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypePseudoMetricSpace