English
For δ > 0 and E, the indicator of E with value 1 is ≤ thickenedIndicator δ E.
Русский
Для δ > 0 и E индикатор E значением 1 не превосходит thickenedIndicator δ E.
LaTeX
$$$\forall δ>0,\; E:\; (E\text{-indicator})(x) \le \operatorname{thickenedIndicator}(δ,E)(x) \quad \text{for all } x$$$
Lean4
theorem indicator_le_thickenedIndicator {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) :
(E.indicator fun _ => (1 : ℝ≥0)) ≤ thickenedIndicator δ_pos E :=
by
intro a
by_cases h : a ∈ E
· simp only [h, indicator_of_mem, thickenedIndicator_one δ_pos E h, le_refl]
· simp only [h, indicator_of_notMem, not_false_iff, zero_le]