Equality_of_Relations
Provedequalityproofwikirelation-theory
Two relations R₁ and R₂ on the same domain and codomain are equal if and only if they contain the same pairs.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Equality_of_Relations {α : Type _} {β : Type _} (R₁ R₂ : α → β → Prop) : R₁ = R₂ ↔ ∀ a b, R₁ a b ↔ R₂ a b := by sorrySource