case mp
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1

case mpr
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.closedBall 0 1
constructor
case mp
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → ∃ a, s ⊆ a • Metric.closedBall 0 1
case mp
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1
rw [isBounded_iff_subset_smul_ball 𝕜]
no goals
case mp
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → ∃ a, s ⊆ a • Metric.closedBall 0 1
exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall
case mpr
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsVonNBounded 𝕜 s
case mpr
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s
rw [← isVonNBounded_iff 𝕜]
case mpr.intro
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.closedBall 0 1
⊢ Bornology.IsVonNBounded 𝕜 s
case mpr
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsVonNBounded 𝕜 s
rintro ⟨a, ha⟩
no goals
case mpr.intro
𝕜 : Type u_2
𝕜' : Type ?u.270507
E : Type u_1
E' : Type ?u.270513
F : Type ?u.270516
ι : Type ?u.270519
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.closedBall 0 1
⊢ Bornology.IsVonNBounded 𝕜 s
exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha