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