Theorems · Definition · general topology

thickenedIndicator

{α : Type u_1} → [inst : PseudoEMetricSpace α] → {δ : ℝ} → 0 < δ → Set α → BoundedContinuousFunction α NNReal

The δ-thickened indicator of a set E is the function that equals 1 on E and 0 outside a δ-thickening of E and interpolates (continuously) between these values using infEDist _ E. thickenedIndicator is the (bundled) bounded continuous function with ℝ≥0-values. See thickenedIndicatorAux for the unbundled ℝ≥0∞-valued function.

Defined in

Mathlib.Topology.MetricSpace.ThickenedIndicator

Cited by

23 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace