case intro
ι : Type ?u.89294
R : Type ?u.89297
R' : Type ?u.89300
E : Type u_1
F : Type ?u.89306
G : Type ?u.89309
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝¹ y : E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => ↑p y + ↑q (x✝ / y)) x
ι : Type ?u.89294
R : Type ?u.89297
R' : Type ?u.89300
E : Type u_1
F : Type ?u.89306
G : Type ?u.89309
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y : E
p q : GroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y => ↑p y + ↑q (x / y))
rintro _ ⟨x, rfl⟩
case intro
ι : Type ?u.89294
R : Type ?u.89297
R' : Type ?u.89300
E : Type u_1
F : Type ?u.89306
G : Type ?u.89309
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝¹ y : E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ / x)
case intro
ι : Type ?u.89294
R : Type ?u.89297
R' : Type ?u.89300
E : Type u_1
F : Type ?u.89306
G : Type ?u.89309
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝¹ y : E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => ↑p y + ↑q (x✝ / y)) x
dsimp
no goals
case intro
ι : Type ?u.89294
R : Type ?u.89297
R' : Type ?u.89300
E : Type u_1
F : Type ?u.89306
G : Type ?u.89309
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝¹ y : E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ / x)
positivity