case intro
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
R : ℝ
hR : ∀ (x : E), x ∈ s → ‖x‖ ≤ R
⊢ Bounded (c • s)
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
⊢ Bounded (c • s)
obtain ⟨R, hR⟩ : ∃ R : ℝ, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le
case intro
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
R : ℝ
hR : ∀ (x : E), x ∈ s → ‖x‖ ≤ R
z : E
hz : z ∈ c • s
⊢ ‖z‖ ≤ ‖c‖ * R
case intro
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
R : ℝ
hR : ∀ (x : E), x ∈ s → ‖x‖ ≤ R
⊢ Bounded (c • s)
refine' bounded_iff_forall_norm_le.2 ⟨‖c‖ * R, fun z hz => _⟩
case intro.intro.intro
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
R : ℝ
hR : ∀ (x : E), x ∈ s → ‖x‖ ≤ R
y : E
ys : y ∈ s
hz : c • y ∈ c • s
⊢ ‖c • y‖ ≤ ‖c‖ * R
case intro
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
R : ℝ
hR : ∀ (x : E), x ∈ s → ‖x‖ ≤ R
z : E
hz : z ∈ c • s
⊢ ‖z‖ ≤ ‖c‖ * R
obtain ⟨y, ys, rfl⟩ : ∃ y : E, y ∈ s ∧ c • y = z := mem_smul_set.1 hz
no goals
case intro.intro.intro
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
hs : Bounded s
c : 𝕜
R : ℝ
hR : ∀ (x : E), x ∈ s → ‖x‖ ≤ R
y : E
ys : y ∈ s
hz : c • y ∈ c • s
⊢ ‖c • y‖ ≤ ‖c‖ * R
calc
  ‖c • y‖ = ‖c‖ * ‖y‖ := norm_smul _ _
  _ ≤ ‖c‖ * R := mul_le_mul_of_nonneg_left (hR y ys) (norm_nonneg _)