English
For any δ > 0 and E, the function thickenedIndicator δ_pos E x is ≤ 1 for all x.
Русский
Для любого δ > 0 и любого E функция thickenedIndicator δ_pos E x не превосходит 1 для всех x.
LaTeX
$$$\forall δ>0,\; E\subseteq \alpha:\; \operatorname{thickenedIndicator}(δ,E)(x) \le 1 \text{ for all } x$$$
Lean4
theorem thickenedIndicator_le_one {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α) : thickenedIndicator δ_pos E x ≤ 1 :=
by
rw [thickenedIndicator.coeFn_eq_comp]
simpa using (toNNReal_le_toNNReal (by finiteness) one_ne_top).mpr (thickenedIndicatorAux_le_one δ E x)