theorem Set.mem_image
theorem Set.mem_image: ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y
theorem Set.mem_image
theorem Set.mem_image: ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y