thickenedIndicatorAux_mono — Mathlib

English

If δ1 ≤ δ2, then thickenedIndicatorAux δ1 E ≤ thickenedIndicatorAux δ2 E (pointwise).

Русский

Если δ1 ≤ δ2, то thickenedIndicatorAux δ1 E ≤ thickenedIndicatorAux δ2 E по каждому x.

LaTeX

$$$\forall δ_1, δ_2 \in \mathbb{R},\; δ_1 \le δ_2,\; \forall E \subseteq \alpha,\; \forall x \in \alpha:\; \operatorname{thickenedIndicatorAux}(δ_1,E)(x) \le \operatorname{thickenedIndicatorAux}(δ_2,E)(x)$$$

Lean4

theorem thickenedIndicatorAux_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) :
    thickenedIndicatorAux δ₁ E ≤ thickenedIndicatorAux δ₂ E := fun _ =>
  tsub_le_tsub (@rfl ℝ≥0∞ 1).le (ENNReal.div_le_div rfl.le (ofReal_le_ofReal hle))

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