thickening_mono — Mathlib

English

If δ₁ ≤ δ₂, then thickening δ₁ E ⊆ thickening δ₂ E.

Русский

Если δ₁ ≤ δ₂, то thickening δ₁ E ⊆ thickening δ₂ E.

LaTeX

$$$δ₁ ≤ δ₂ \\Rightarrow thickening\\,δ₁\\,E \\subseteq thickening\\,δ₂\\,E$$$

Lean4

/-- The (open) thickening `Metric.thickening δ E` of a fixed subset `E` is an increasing function of
the thickening radius `δ`. -/
@[gcongr]
theorem thickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : thickening δ₁ E ⊆ thickening δ₂ E :=
  preimage_mono (Iio_subset_Iio (ENNReal.ofReal_le_ofReal hle))

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