Image_of_Union_under_Relation
Provedimage-of-union-under-relationproofwikirelation-theoryset-union
Let R be a relation from S to T. Let S₁ and S₂ be subsets of S. Then the image of (S₁ ∪ S₂) under R equals the union of the images of S₁ and S₂ under R.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Image
Formal statement
theorem Image_of_Union_under_Relation {α β : Type _} (r : Set (α × β)) (S₁ S₂ : Set α) : (fun p : α × β => p.2) '' {p ∈ r | p.1 ∈ S₁ ∪ S₂} = (fun p : α × β => p.2) '' {p ∈ r | p.1 ∈ S₁} ∪ (fun p : α × β => p.2) '' {p ∈ r | p.1 ∈ S₂} := by sorrySource