thickening — Mathlib

English

If E is bounded, then thickening δ E is bounded for any δ.

Русский

Если E ограничено, то для любого δ thickening δ E ограничено.

LaTeX

$$IsBounded(E) → IsBounded(thickening δ E)$$

Lean4

protected theorem _root_.Bornology.IsBounded.thickening {δ : ℝ} {E : Set X} (h : IsBounded E) :
    IsBounded (thickening δ E) := by
  rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
  · simp
  · refine (isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩
    calc
      dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
      _ ≤ δ + diam E := add_le_add_right ((mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy).le _

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