Image_of_Singleton_under_Relation
Provedproofwikirelation-theorysingletons
The image of a singleton {s} under a function f equals the singleton {f(s)}: f '' {s} = {f s}
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Image_of_Singleton_under_Relation {α : Type _} {β : Type _} (f : α → β) (s : α) : f '' {s} = {f s} := by sorrySource