indicator_le_thickenedIndicator — Mathlib

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]

Похожие утверждения