Theorems · Definition · general topology

thickenedIndicatorAux

{α : Type u_1} → [PseudoEMetricSpace α] → ℝ → Set α → α → ENNReal

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. thickenedIndicatorAux is the unbundled ℝ≥0∞-valued function. See thickenedIndicator for the (bundled) bounded continuous function with ℝ≥0-values.

Defined in

Mathlib.Topology.MetricSpace.ThickenedIndicator

Cited by

21 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace