Inverse_of_Inverse_Relation
Provedinverse-relationsproofwiki
The inverse of the inverse of a relation R is R itself: (R⁻¹)⁻¹ = R
Preamble
import Mathlib.Data.Set.Prod import Mathlib.Data.Set.Function
Formal statement
theorem Inverse_of_Inverse_Relation {α : Type _} {β : Type _} (R : Set (α × β)) : (Prod.swap '' (Prod.swap '' R)) = R := by sorrySource