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)