Theorems · Theorem · general topology

closedBall_pi

∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b)
  {r : ℝ}, 0 ≤ r → Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r

A closed ball in a product space is a product of closed balls. See also closedBall_pi' for a version assuming Nonempty β instead of 0 ≤ r.

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Pi

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypePseudoMetricSpace