cthickening_subset_thickening' — Mathlib

English

If δ2 > 0 and δ1 < δ2, then cthickening δ1 E ⊆ thickening δ2 E.

Русский

Если δ2 > 0 и δ1 < δ2, то cthickening δ1 E ⊆ thickening δ2 E.

LaTeX

$$$ δ_2 > 0 \land δ_1 < δ_2 \Rightarrow cthickening δ_1 E \subseteq thickening δ_2 E $$$

Lean4

/-- The closed thickening `Metric.cthickening δ₁ E` is contained in the open thickening
`Metric.thickening δ₂ E` if the radius of the latter is positive and larger. -/
theorem cthickening_subset_thickening' {δ₁ δ₂ : ℝ} (δ₂_pos : 0 < δ₂) (hlt : δ₁ < δ₂) (E : Set α) :
    cthickening δ₁ E ⊆ thickening δ₂ E := fun _ hx =>
  lt_of_le_of_lt hx.out ((ENNReal.ofReal_lt_ofReal_iff δ₂_pos).mpr hlt)

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