cthickening — Mathlib

English

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

Русский

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

LaTeX

$$IsBounded E → IsBounded (cthickening δ E)$$

Lean4

theorem _root_.Bornology.IsBounded.cthickening {α : Type*} [PseudoMetricSpace α] {δ : ℝ} {E : Set α} (h : IsBounded E) :
    IsBounded (cthickening δ E) :=
  by
  have : IsBounded (thickening (max (δ + 1) 1) E) := h.thickening
  apply this.subset
  exact
    cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _)) ((lt_add_one _).trans_le (le_max_left _ _))
      _

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