thickening_subset_of_subset — Mathlib

English

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

Русский

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

LaTeX

$$$E₁ ⊆ E₂ \\Rightarrow thickening\\,δ\\,E₁ ⊆ thickening\\,δ\\,E₂$$$

Lean4

/-- The (open) thickening `Metric.thickening δ E` with a fixed thickening radius `δ` is
an increasing function of the subset `E`. -/
theorem thickening_subset_of_subset (δ : ℝ) {E₁ E₂ : Set α} (h : E₁ ⊆ E₂) : thickening δ E₁ ⊆ thickening δ E₂ :=
  fun _ hx => lt_of_le_of_lt (infEdist_anti h) hx

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