𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, s ⊆ Metric.closedBall 0 r
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
rw [← Metric.bounded_iff_isBounded, Metric.bounded_iff_subset_ball (0 : E)]
case mp
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s → ∃ r, s ⊆ Metric.closedBall 0 r

case mpr
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ r, s ⊆ Metric.closedBall 0 r) → Bornology.IsVonNBounded 𝕜 s
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, s ⊆ Metric.closedBall 0 r
constructor
case mp
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
case mp
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s → ∃ r, s ⊆ Metric.closedBall 0 r
intro h
case mp.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
case mp
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
rcases h (Metric.ball_mem_nhds 0 zero_lt_one) with ⟨ρ, hρ, hρball⟩
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
case mp.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ a • Metric.ball 0 1
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
specialize hρball a ha.le
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 ‖a‖
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ a • Metric.ball 0 1
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha),
  ball_normSeminorm, mul_one] at hρball
no goals
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 ‖a‖
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
exact ⟨‖a‖, hρball.trans Metric.ball_subset_closedBall⟩
no goals
case mpr
𝕜 : Type u_2
𝕜' : Type ?u.246833
E : Type u_1
E' : Type ?u.246839
F : Type ?u.246842
ι : Type ?u.246845
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ r, s ⊆ Metric.closedBall 0 r) → Bornology.IsVonNBounded 𝕜 s
exact fun ⟨C, hC⟩ => (isVonNBounded_closedBall 𝕜 E C).subset hC