no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ ↑(thickenedIndicator δ_pos E) x = 1
rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, one_toNNReal]