Preimage_of_Image_under_Left_Total_Relation_is_Superset
Provedcomposite-relationspreimages-under-relationsproofwiki
For any function f and set A, A ⊆ f ⁻¹' (f '' A), i.e., the preimage of the image is a superset of the original set.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Preimage_of_Image_under_Left_Total_Relation_is_Superset {α : Type _} {β : Type _} (f : α → β) (A : Set α) : A ⊆ f ⁻¹' (f '' A) := by sorrySource