Theorems · Definition · general topology

Metric.thickening

{α : Type u} → [PseudoEMetricSpace α] → ℝ → Set α → Set α

The (open) δ-thickening Metric.thickening δ E of a subset E in a pseudo emetric space consists of those points that are at distance less than δ from some point of E.

Defined in

Mathlib.Topology.MetricSpace.Thickening

Cited by

130 results in Mathlib

Foundations

Depth 148 from the axioms, rests on 3,163 definitions · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace