Image_of_Empty_Set_is_Empty_Set
Provedempty-setproofwikirelation-theory
The image of the empty set under any function is the empty set: f '' ∅ = ∅
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Image_of_Empty_Set_is_Empty_Set {α : Type _} {β : Type _} (f : α → β) : f '' (∅ : Set α) = ∅ := by sorrySource