cthickening_subset_of_subset — Mathlib

English

If E1 ⊆ E2 then cthickening δ E1 ⊆ cthickening δ E2.

Русский

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

LaTeX

$$$ E_1 \subseteq E_2 \Rightarrow cthickening δ E_1 \subseteq cthickening δ E_2 $$$

Lean4

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

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