Domain_of_Composite_Relation
Provedcomposite-relationsproofwiki
The image of a set under a composite function equals the iterated image: (g ∘ f) '' A = g '' (f '' A)
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Domain_of_Composite_Relation {α : Type _} {β : Type _} {γ : Type _} (f : α → β) (g : β → γ) (A : Set α) : (g ∘ f) '' A = g '' (f '' A) := by sorrySource