Theorems · Theorem · general topology

thickenedIndicator_tendsto_indicator_closure

∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δseq : ℕ → ℝ} (δseq_pos : ∀ (n : ℕ), 0 < δseq n),
  Filter.Tendsto δseq Filter.atTop (nhds 0) →
    ∀ (E : Set α),
      Filter.Tendsto (fun n => ⇑(thickenedIndicator ⋯ E)) Filter.atTop (nhds ((closure E).indicator fun x => 1))

As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends pointwise to the indicator function of the closure of E. Note: This version is for the bundled bounded continuous functions, but the topology is not the topology on α →ᵇ ℝ≥0. Coercions to functions α → ℝ≥0 are done first, so the topology instance is the product topology (the topology of pointwise convergence).

Defined in

Mathlib.Topology.MetricSpace.ThickenedIndicator

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace