no goals
𝓕 : Type ?u.99872
𝕜 : Type ?u.99875
α : Type ?u.99878
ι : Type ?u.99881
κ : Type ?u.99884
E : Type u_1
F : Type ?u.99890
G : Type ?u.99893
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hs : Bounded s
R₀ : ℝ
hR₀ : ∀ (x : E), x ∈ s → ‖x‖ ≤ R₀
⊢ max R₀ 1 > 0
positivity