Image_of_Intersection_under_One_to_Many_Relation
Provedproofwikirelation-theoryset-intersection
Let R ⊆ S × T be a relation. Then for all S₁, S₂ ⊆ S: R[S₁ ∩ S₂] = R[S₁] ∩ R[S₂] iff R is one-to-many. For a mapping (which is many-to-one), this holds iff f is injective.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Image_of_Intersection_under_One_to_Many_Relation {α β : Type _} {f : α → β} (hf : Function.Injective f) (A B : Set α) : f '' (A ∩ B) = f '' A ∩ f '' B := by sorrySource