R : Type ?u.1248543
R' : Type ?u.1248546
𝕜 : Type u_2
𝕜₂ : Type ?u.1248552
𝕜₃ : Type ?u.1248555
𝕝 : Type ?u.1248558
E : Type u_1
E₂ : Type ?u.1248564
E₃ : Type ?u.1248567
F : Type ?u.1248570
G : Type ?u.1248573
ι : Type ?u.1248576
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : y ∈ closedBall p 0 (r - ↑p x)
⊢ y ∈ closedBall p x r
R : Type ?u.1248543
R' : Type ?u.1248546
𝕜 : Type u_2
𝕜₂ : Type ?u.1248552
𝕜₃ : Type ?u.1248555
𝕝 : Type ?u.1248558
E : Type u_1
E₂ : Type ?u.1248564
E₃ : Type ?u.1248567
F : Type ?u.1248570
G : Type ?u.1248573
ι : Type ?u.1248576
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
⊢ Absorbent 𝕜 (closedBall p x r)
refine' (p.absorbent_closedBall_zero <| sub_pos.2 hpr).subset fun y hy => _
R : Type ?u.1248543
R' : Type ?u.1248546
𝕜 : Type u_2
𝕜₂ : Type ?u.1248552
𝕜₃ : Type ?u.1248555
𝕝 : Type ?u.1248558
E : Type u_1
E₂ : Type ?u.1248564
E₃ : Type ?u.1248567
F : Type ?u.1248570
G : Type ?u.1248573
ι : Type ?u.1248576
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : ↑p y ≤ r - ↑p x
⊢ y ∈ closedBall p x r
R : Type ?u.1248543
R' : Type ?u.1248546
𝕜 : Type u_2
𝕜₂ : Type ?u.1248552
𝕜₃ : Type ?u.1248555
𝕝 : Type ?u.1248558
E : Type u_1
E₂ : Type ?u.1248564
E₃ : Type ?u.1248567
F : Type ?u.1248570
G : Type ?u.1248573
ι : Type ?u.1248576
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : y ∈ closedBall p 0 (r - ↑p x)
⊢ y ∈ closedBall p x r
rw [p.mem_closedBall_zero] at hy
no goals
R : Type ?u.1248543
R' : Type ?u.1248546
𝕜 : Type u_2
𝕜₂ : Type ?u.1248552
𝕜₃ : Type ?u.1248555
𝕝 : Type ?u.1248558
E : Type u_1
E₂ : Type ?u.1248564
E₃ : Type ?u.1248567
F : Type ?u.1248570
G : Type ?u.1248573
ι : Type ?u.1248576
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : ↑p y ≤ r - ↑p x
⊢ y ∈ closedBall p x r
exact p.mem_closedBall.2 ((map_sub_le_add p _ _).trans <| add_le_of_le_sub_right hy)