thickenedIndicator_subset — Mathlib

English

If E1 ⊆ E2, then thickenedIndicator δ E1 ≤ thickenedIndicator δ E2 as functions.

Русский

Если E1 ⊆ E2, то thickenedIndicator δ E1 ≤ thickenedIndicator δ E2 как функции.

LaTeX

$$$\forall δ \in \mathbb{R},\; E_1 \subseteq E_2:\; \operatorname{thickenedIndicator}(δ,E_1) ≤ \operatorname{thickenedIndicator}(δ,E_2)$$$

Lean4

theorem thickenedIndicator_subset {δ : ℝ} (δ_pos : 0 < δ) {E₁ E₂ : Set α} (subset : E₁ ⊆ E₂) :
    ⇑(thickenedIndicator δ_pos E₁) ≤ thickenedIndicator δ_pos E₂ := fun x =>
  (toNNReal_le_toNNReal (by finiteness) (by finiteness)).mpr (thickenedIndicatorAux_subset δ subset x)

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