cthickening_mono — Mathlib

English

If δ1 ≤ δ2 then cthickening δ1 E ⊆ cthickening δ2 E (monotonicity in radius).

Русский

Если δ1 ≤ δ2, то cthickening δ1 E ⊆ cthickening δ2 E (монотонность по радиусу).

LaTeX

$$$ δ_1 ≤ δ_2 \Rightarrow cthickening δ_1 E \subseteq cthickening δ_2 E $$$

Lean4

/-- The closed thickening `Metric.cthickening δ E` of a fixed subset `E` is an increasing function
of the thickening radius `δ`. -/
theorem cthickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : cthickening δ₁ E ⊆ cthickening δ₂ E :=
  preimage_mono (Iic_subset_Iic.mpr (ENNReal.ofReal_le_ofReal hle))

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