Image_of_Intersection_under_Injection
Provedinjectionsproofwikiset-intersection
Let f: S → T be an injection and let A, B ⊆ S. Then f[A ∩ B] = f[A] ∩ f[B].
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Image_of_Intersection_under_Injection {α β : Type _} {f : α → β} (hf : Function.Injective f) (A B : Set α) : f '' (A ∩ B) = f '' A ∩ f '' B := by sorrySource