Theorems · Theorem · general topology

Metric.cthickening_eq_biUnion_closedBall

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

Defined in

Mathlib.Topology.MetricSpace.Thickening

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceProperSpace