Image_of_Intersection_under_Relation
Provedproofwikirelation-theoryset-intersection
Let R be a relation from S to T. Let S₁ and S₂ be subsets of S. Then the image of the intersection of S₁ and S₂ is a subset of the intersection of their images.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Image
Formal statement
theorem Image_of_Intersection_under_Relation {α β : Type _} (f : α → β) (S₁ S₂ : Set α) : f '' (S₁ ∩ S₂) ⊆ f '' S₁ ∩ f '' S₂ := by sorrySource