case intro
R : Type ?u.587125
R' : Type ?u.587128
𝕜 : Type u_2
𝕜₂ : Type ?u.587134
𝕜₃ : Type ?u.587137
𝕝 : Type ?u.587140
E : Type u_1
E₂ : Type ?u.587146
E₃ : Type ?u.587149
F : Type ?u.587152
G : Type ?u.587155
ι : Type ?u.587158
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ (fun u => ↑p u + ↑q (x✝ - u)) x
R : Type ?u.587125
R' : Type ?u.587128
𝕜 : Type u_2
𝕜₂ : Type ?u.587134
𝕜₃ : Type ?u.587137
𝕝 : Type ?u.587140
E : Type u_1
E₂ : Type ?u.587146
E₃ : Type ?u.587149
F : Type ?u.587152
G : Type ?u.587155
ι : Type ?u.587158
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
⊢ 0 ∈ lowerBounds (range fun u => ↑p u + ↑q (x - u))
rintro _ ⟨x, rfl⟩
case intro
R : Type ?u.587125
R' : Type ?u.587128
𝕜 : Type u_2
𝕜₂ : Type ?u.587134
𝕜₃ : Type ?u.587137
𝕝 : Type ?u.587140
E : Type u_1
E₂ : Type ?u.587146
E₃ : Type ?u.587149
F : Type ?u.587152
G : Type ?u.587155
ι : Type ?u.587158
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ - x)
case intro
R : Type ?u.587125
R' : Type ?u.587128
𝕜 : Type u_2
𝕜₂ : Type ?u.587134
𝕜₃ : Type ?u.587137
𝕝 : Type ?u.587140
E : Type u_1
E₂ : Type ?u.587146
E₃ : Type ?u.587149
F : Type ?u.587152
G : Type ?u.587155
ι : Type ?u.587158
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ (fun u => ↑p u + ↑q (x✝ - u)) x
dsimp
no goals
case intro
R : Type ?u.587125
R' : Type ?u.587128
𝕜 : Type u_2
𝕜₂ : Type ?u.587134
𝕜₃ : Type ?u.587137
𝕝 : Type ?u.587140
E : Type u_1
E₂ : Type ?u.587146
E₃ : Type ?u.587149
F : Type ?u.587152
G : Type ?u.587155
ι : Type ?u.587158
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ - x)
positivity