Inverse_of_Composite_Relation
Provedcomposite-relationsinverse-relationsproofwiki
Let R₂ ∘ R₁ be the composite of two relations. Then (R₂ ∘ R₁)⁻¹ = R₁⁻¹ ∘ R₂⁻¹. Formalized here as the image of a composite equals the iterated image.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Inverse_of_Composite_Relation {α : Type _} {β : Type _} {γ : Type _} (f : α → β) (g : β → γ) (S : Set α) : (g ∘ f) '' S = g '' (f '' S) := by sorrySource