Image_of_Subset_under_Relation_is_Subset_of_Image
Provedproofwikirelation-theorysubsets
If A ⊆ B, then the image of A under f is a subset of the image of B: A ⊆ B → f '' A ⊆ f '' B
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Image_of_Subset_under_Relation_is_Subset_of_Image {α : Type _} {β : Type _} (f : α → β) (A B : Set α) (h : A ⊆ B) : f '' A ⊆ f '' B := by sorrySource