case h
R : Type ?u.1158991
R' : Type ?u.1158994
𝕜 : Type u_1
𝕜₂ : Type ?u.1159000
𝕜₃ : Type ?u.1159003
𝕝 : Type ?u.1159006
E : Type u_2
E₂ : Type ?u.1159012
E₃ : Type ?u.1159015
F : Type ?u.1159018
G : Type ?u.1159021
ι : Type ?u.1159024
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ x✝ ∈ closedBall p x r ↔ x✝ ∈ ∅
R : Type ?u.1158991
R' : Type ?u.1158994
𝕜 : Type u_1
𝕜₂ : Type ?u.1159000
𝕜₃ : Type ?u.1159003
𝕝 : Type ?u.1159006
E : Type u_2
E₂ : Type ?u.1159012
E₃ : Type ?u.1159015
F : Type ?u.1159018
G : Type ?u.1159021
ι : Type ?u.1159024
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
⊢ closedBall p x r = ∅
ext
case h
R : Type ?u.1158991
R' : Type ?u.1158994
𝕜 : Type u_1
𝕜₂ : Type ?u.1159000
𝕜₃ : Type ?u.1159003
𝕝 : Type ?u.1159006
E : Type u_2
E₂ : Type ?u.1159012
E₃ : Type ?u.1159015
F : Type ?u.1159018
G : Type ?u.1159021
ι : Type ?u.1159024
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ r < ↑p (x✝ - x)
case h
R : Type ?u.1158991
R' : Type ?u.1158994
𝕜 : Type u_1
𝕜₂ : Type ?u.1159000
𝕜₃ : Type ?u.1159003
𝕝 : Type ?u.1159006
E : Type u_2
E₂ : Type ?u.1159012
E₃ : Type ?u.1159015
F : Type ?u.1159018
G : Type ?u.1159021
ι : Type ?u.1159024
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ x✝ ∈ closedBall p x r ↔ x✝ ∈ ∅
rw [Seminorm.mem_closedBall, Set.mem_empty_iff_false, iff_false_iff, not_le]
no goals
case h
R : Type ?u.1158991
R' : Type ?u.1158994
𝕜 : Type u_1
𝕜₂ : Type ?u.1159000
𝕜₃ : Type ?u.1159003
𝕝 : Type ?u.1159006
E : Type u_2
E₂ : Type ?u.1159012
E₃ : Type ?u.1159015
F : Type ?u.1159018
G : Type ?u.1159021
ι : Type ?u.1159024
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ r < ↑p (x✝ - x)
exact hr.trans_le (map_nonneg _ _)