case intro.intro
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ closedBall p 0 r
h : (fun x => k • x) y = x
⊢ x ∈ closedBall p 0 (‖k‖ * r)
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
⊢ k • closedBall p 0 r ⊆ closedBall p 0 (‖k‖ * r)
rintro x ⟨y, hy, h⟩
case intro.intro
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ closedBall p 0 r
h : (fun x => k • x) y = x
⊢ ‖k‖ * ↑p y ≤ ‖k‖ * r
case intro.intro
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ closedBall p 0 r
h : (fun x => k • x) y = x
⊢ x ∈ closedBall p 0 (‖k‖ * r)
rw [Seminorm.mem_closedBall_zero, ← h, map_smul_eq_mul]
case intro.intro
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : ↑p y ≤ r
h : (fun x => k • x) y = x
⊢ ‖k‖ * ↑p y ≤ ‖k‖ * r
case intro.intro
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ closedBall p 0 r
h : (fun x => k • x) y = x
⊢ ‖k‖ * ↑p y ≤ ‖k‖ * r
rw [Seminorm.mem_closedBall_zero] at hy
no goals
case intro.intro
R : Type ?u.1191905
R' : Type ?u.1191908
𝕜 : Type u_1
𝕜₂ : Type ?u.1191914
𝕜₃ : Type ?u.1191917
𝕝 : Type ?u.1191920
E : Type u_2
E₂ : Type ?u.1191926
E₃ : Type ?u.1191929
F : Type ?u.1191932
G : Type ?u.1191935
ι : Type ?u.1191938
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : ↑p y ≤ r
h : (fun x => k • x) y = x
⊢ ‖k‖ * ↑p y ≤ ‖k‖ * r
gcongr