Theorems · Theorem · general topology

IsCompact.cthickening_eq_biUnion_closedBall

∀ {α : Type u_2} [inst : PseudoMetricSpace α] {δ : ℝ} {E : Set α},
  IsCompact E → 0 ≤ δ → Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ

The closed thickening of a compact set E is the union of the balls Metric.closedBall x δ over x ∈ E. See also Metric.cthickening_eq_biUnion_closedBall.

Defined in

Mathlib.Topology.MetricSpace.Thickening

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace