Image_of_Intersection_under_Mapping
Provedmapping-theoryproofwikiset-intersection
Let f: S → T be a mapping and let S₁ and S₂ be subsets of S. Then f[S₁ ∩ S₂] ⊆ f[S₁] ∩ f[S₂].
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Image_of_Intersection_under_Mapping {α β : Type _} (f : α → β) (A B : Set α) : f '' (A ∩ B) ⊆ f '' A ∩ f '' B := by sorrySource