ι : Sort ?u.109564
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
this : Bounded (thickening (max (δ + 1) 1) E)
⊢ Bounded (Metric.cthickening δ E)
ι : Sort ?u.109564
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
⊢ Bounded (Metric.cthickening δ E)
have : Bounded (thickening (max (δ + 1) 1) E) := h.thickening
ι : Sort ?u.109564
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
this : Bounded (thickening (max (δ + 1) 1) E)
⊢ Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E
ι : Sort ?u.109564
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
this : Bounded (thickening (max (δ + 1) 1) E)
⊢ Bounded (Metric.cthickening δ E)
apply Bounded.mono _ this
no goals
ι : Sort ?u.109564
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
this : Bounded (thickening (max (δ + 1) 1) E)
⊢ Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E
exact cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _))
  ((lt_add_one _).trans_le (le_max_left _ _)) _