Relation_is_Antireflexive_iff_Disjoint_from_Diagonal_Relation
Provedproofwikireflexive-relations
A relation R on S is antireflexive if and only if the diagonal relation Δ_S and R are disjoint.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Prod
Formal statement
theorem Relation_is_Antireflexive_iff_Disjoint_from_Diagonal_Relation {α : Type _} (R : α → α → Prop) : (∀ x, ¬ R x x) ↔ ({p : α × α | R p.1 p.2} ∩ {p : α × α | p.1 = p.2} = ∅) := by sorrySource