Complement_of_Symmetric_Relation
Provedproofwikirelative-complementsymmetric-relations
If R is a symmetric relation on S, then its complement is also symmetric.
Preamble
import Mathlib.Logic.Relation
Formal statement
theorem Complement_of_Symmetric_Relation {α : Type _} (R : α → α → Prop) (hR : Symmetric R) : Symmetric (fun a b => ¬ R a b) := by sorrySource