thickenedIndicator_mono — Mathlib

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

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