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