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