indicator_le_thickenedIndicatorAux

English

For all δ ∈ ℝ and E ⊆ α, the indicator of E with value 1 is ≤ thickenedIndicatorAux δ E.

Русский

Для любого δ ∈ ℝ и любого E ⊆ α индикатор E со значением 1 не превосходит thickenedIndicatorAux δ E.

LaTeX

$$$\forall δ \in \mathbb{R},\; E \subseteq \alpha:\; (E\text{-indicator})(x) \le \operatorname{thickenedIndicatorAux}(δ,E)(x) \text{ for all } x$$$

Lean4

theorem indicator_le_thickenedIndicatorAux (δ : ℝ) (E : Set α) :
    (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ thickenedIndicatorAux δ E :=
  by
  intro a
  by_cases h : a ∈ E
  · simp only [h, indicator_of_mem, thickenedIndicatorAux_one δ E h, le_refl]
  · simp only [h, indicator_of_notMem, not_false_iff, zero_le]

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