α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ ↑(thickenedIndicator δ_pos E) x ≤ 1
rw [thickenedIndicator.coeFn_eq_comp]
no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1
simpa using (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne one_ne_top).mpr
  (thickenedIndicatorAux_le_one δ E x)