no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ¬x ∈ thickening δ E
⊢ ↑(thickenedIndicator δ_pos E) x = 0
rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, zero_toNNReal]