cthickening_subset_thickening — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem cthickening_subset_thickening {δ₁ : ℝ≥0} {δ₂ : ℝ} (hlt : (δ₁ : ℝ) < δ₂) (E : Set α) :
    cthickening δ₁ E ⊆ thickening δ₂ E := fun _ hx =>
  hx.out.trans_lt ((ENNReal.ofReal_lt_ofReal_iff (lt_of_le_of_lt δ₁.prop hlt)).mpr hlt)

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