thickenedIndicatorAux_subset — Mathlib

English

If E1 ⊆ E2, then thickenedIndicatorAux δ E1 ≤ thickenedIndicatorAux δ E2.

Русский

Если E1 ⊆ E2, то thickenedIndicatorAux δ E1 ≤ thickenedIndicatorAux δ E2.

LaTeX

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

Lean4

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

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