Theorems · Theorem · general topology

thickenedIndicator_zero

∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α},
  x ∉ Metric.thickening δ E → (thickenedIndicator δ_pos E) x = 0

Defined in

Mathlib.Topology.MetricSpace.ThickenedIndicator

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace