Antireflexive_and_Transitive_Relation_is_Asymmetric
Provedproofwikireflexive-relationssymmetric-relationstransitive-relations
Let R be a relation which is antireflexive and transitive. Then R is also asymmetric.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Antireflexive_and_Transitive_Relation_is_Asymmetric {α : Type _} (R : α → α → Prop) (hIrr : ∀ x, ¬ R x x) (hTrans : ∀ x y z, R x y → R y z → R x z) : ∀ x y, R x y → ¬ R y x := by sorrySource