no goals
α : Type u_2
β : Type u_1
γ : Type ?u.25263
δ : Type ?u.25266
e : LocalEquiv α β
e' : LocalEquiv β γ
p : β → Prop
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (↑e x)
rw [← image_source_eq_target, ball_image_iff]