case intro
ι : Type ?u.158932
R : Type ?u.158935
R' : Type ?u.158938
E : Type u_1
F : Type ?u.158944
G : Type ?u.158947
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝¹ y : E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => ↑p y + ↑q (x✝ - y)) x
ι : Type ?u.158932
R : Type ?u.158935
R' : Type ?u.158938
E : Type u_1
F : Type ?u.158944
G : Type ?u.158947
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝ y : E
p q : NonarchAddGroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y => ↑p y + ↑q (x - y))
rintro _ ⟨x, rfl⟩
case intro
ι : Type ?u.158932
R : Type ?u.158935
R' : Type ?u.158938
E : Type u_1
F : Type ?u.158944
G : Type ?u.158947
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝¹ y : E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ - x)
case intro
ι : Type ?u.158932
R : Type ?u.158935
R' : Type ?u.158938
E : Type u_1
F : Type ?u.158944
G : Type ?u.158947
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝¹ y : E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => ↑p y + ↑q (x✝ - y)) x
dsimp
no goals
case intro
ι : Type ?u.158932
R : Type ?u.158935
R' : Type ?u.158938
E : Type u_1
F : Type ?u.158944
G : Type ?u.158947
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝¹ y : E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ - x)
positivity