𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology
rw [Bornology.ext_iff_isBounded]
𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
intro s
𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
rw [Bornology.isBounded_iff_isVonNBounded]
no goals
𝕜 : Type u_2
𝕜' : Type ?u.259865
E : Type u_1
E' : Type ?u.259871
F : Type ?u.259874
ι : Type ?u.259877
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
exact isVonNBounded_iff 𝕜 E s