Symmetric_Transitive_and_Serial_Relation_is_Reflexive
Provedequivalence-relationsproofwikireflexive-relationsserial-relationssymmetric-relationstransitive-relations
Let R be a relation which is symmetric, transitive, and serial. Then R is reflexive.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Symmetric_Transitive_and_Serial_Relation_is_Reflexive {α : Type _} (R : α → α → Prop) (hSym : ∀ x y, R x y → R y x) (hTrans : ∀ x y z, R x y → R y z → R x z) (hSerial : ∀ x, ∃ y, R x y) : ∀ x, R x x := by sorrySource