case h
R : Type ?u.1149982
R' : Type ?u.1149985
𝕜 : Type u_1
𝕜₂ : Type ?u.1149991
𝕜₃ : Type ?u.1149994
𝕝 : Type ?u.1149997
E : Type u_2
E₂ : Type ?u.1150003
E₃ : Type ?u.1150006
F : Type ?u.1150009
G : Type ?u.1150012
ι : Type ?u.1150015
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✝ ∈ ball p x r ↔ x✝ ∈ ∅
R : Type ?u.1149982
R' : Type ?u.1149985
𝕜 : Type u_1
𝕜₂ : Type ?u.1149991
𝕜₃ : Type ?u.1149994
𝕝 : Type ?u.1149997
E : Type u_2
E₂ : Type ?u.1150003
E₃ : Type ?u.1150006
F : Type ?u.1150009
G : Type ?u.1150012
ι : Type ?u.1150015
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
⊢ ball p x r = ∅
ext
case h
R : Type ?u.1149982
R' : Type ?u.1149985
𝕜 : Type u_1
𝕜₂ : Type ?u.1149991
𝕜₃ : Type ?u.1149994
𝕝 : Type ?u.1149997
E : Type u_2
E₂ : Type ?u.1150003
E₃ : Type ?u.1150006
F : Type ?u.1150009
G : Type ?u.1150012
ι : Type ?u.1150015
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.1149982
R' : Type ?u.1149985
𝕜 : Type u_1
𝕜₂ : Type ?u.1149991
𝕜₃ : Type ?u.1149994
𝕝 : Type ?u.1149997
E : Type u_2
E₂ : Type ?u.1150003
E₃ : Type ?u.1150006
F : Type ?u.1150009
G : Type ?u.1150012
ι : Type ?u.1150015
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✝ ∈ ball p x r ↔ x✝ ∈ ∅
rw [Seminorm.mem_ball, Set.mem_empty_iff_false, iff_false_iff, not_lt]
no goals
case h
R : Type ?u.1149982
R' : Type ?u.1149985
𝕜 : Type u_1
𝕜₂ : Type ?u.1149991
𝕜₃ : Type ?u.1149994
𝕝 : Type ?u.1149997
E : Type u_2
E₂ : Type ?u.1150003
E₃ : Type ?u.1150006
F : Type ?u.1150009
G : Type ?u.1150012
ι : Type ?u.1150015
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 (map_nonneg p _)