theorem Set.mem_preimage
theorem Set.mem_preimage: ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ s
theorem Set.mem_preimage
theorem Set.mem_preimage: ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ s