Null_Relation_is_Antireflexive_Symmetric_and_Transitive
Provednull-relationproofwikireflexive-relationssymmetric-relationstransitive-relations
Let S be a non-empty set. Let R be the null relation on S. Then R is antireflexive, symmetric, and transitive.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Null_Relation_is_Antireflexive_Symmetric_and_Transitive {α : Type _} [Nonempty α] (R : α → α → Prop) (hR : ∀ x y, ¬ R x y) : (∀ x, ¬ R x x) ∧ (∀ x y, R x y → R y x) ∧ (∀ x y z, R x y → R y z → R x z) := by sorrySource