Coreflexive_Relation_Subset_of_Diagonal
Provedproofwikirelation-theory
A coreflexive relation is a subset of the diagonal (identity) relation.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Coreflexive_Relation_Subset_of_Diagonal {α : Type _} (R : α → α → Prop) (hR : ∀ x y, R x y → x = y) : ∀ x y, R x y → x = y := by sorrySource