English
If δ1 > 0, δ2 > 0 and δ1 ≤ δ2, then thickenedIndicator δ1 E ≤ thickenedIndicator δ2 E as functions.
Русский
Если δ1 > 0, δ2 > 0 и δ1 ≤ δ2, то thickenedIndicator δ1 E ≤ thickenedIndicator δ2 E как функции.
LaTeX
$$$\forall δ_1, δ_2 \in \mathbb{R}_{>0},\; δ_1 ≤ δ_2:\; \operatorname{thickenedIndicator}(δ_1,E) ≤ \operatorname{thickenedIndicator}(δ_2,E)$$$
Lean4
theorem thickenedIndicator_mono {δ₁ δ₂ : ℝ} (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ ≤ δ₂) (E : Set α) :
⇑(thickenedIndicator δ₁_pos E) ≤ thickenedIndicator δ₂_pos E :=
by
intro x
apply (toNNReal_le_toNNReal (by finiteness) (by finiteness)).mpr
apply thickenedIndicatorAux_mono hle