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 _ _))
_