no goals
α : Type ?u.146221
β : Type ?u.146224
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Set ℝ≥0
⊢ ↑r ∈ upperBounds (some '' s) ↔ r ∈ upperBounds s
simp (config := { contextual := true }) [upperBounds, ball_image_iff, -mem_image, *]