Antitransitive_Relation_is_Antireflexive
Provedproofwikireflexive-relationstransitive-relations
Let R be an antitransitive relation on S. Then R is also antireflexive.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Antitransitive_Relation_is_Antireflexive {α : Type _} (R : α → α → Prop) (hAntiTrans : ∀ x y z, R x y → R y z → ¬ R x z) : ∀ x, ¬ R x x := by sorrySource