Relation_is_Symmetric_and_Antisymmetric_iff_Coreflexive
Provedproofwikireflexive-relationssymmetric-relations
Let R be a relation on S. Then R is both symmetric and antisymmetric if and only if R is coreflexive (i.e., R x y implies x = y).
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Relation_is_Symmetric_and_Antisymmetric_iff_Coreflexive {α : Type _} (R : α → α → Prop) : ((∀ x y, R x y → R y x) ∧ (∀ x y, R x y → R y x → x = y)) ↔ (∀ x y, R x y → x = y) := by sorrySource