feat: port 'section relation' in Init/Logic (#379)

#34 left `section relation` as a TODO. This PR fills it in.

Compare to the Lean 3 version: https://github.com/leanprover-community/lean/blob/741670c439f1ca266bc7fe61ef7212cc9afd9dd8/library/init/logic.lean#L1027-L1062

Author: dwrensha

Mathlib/Init/Logic.lean

@@ -536,7 +536,56 @@ lemma let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β
              a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁; b₁ x) = (let x : α := a₂; b₂ x) :=
 λ h₁ h₂ => Eq.recOn (motive := λ a _ => (let x := a₁; b₁ x) = (let x := a; b₂ x)) h₁ (h₂ a₁)
 
--- TODO: `section relation`
+section relation
+
+variable {α : Sort u} {β : Sort v} (r : β → β → Prop)
+
+/-- Local notation for an arbitrary binary relation `r`. -/
+local infix:50 " ≺ " => r
+
+/-- A reflexive relation relates every element to itself. -/
+def reflexive := ∀ x, x ≺ x
+
+/-- A relation is symmetric if `x ≺ y` implies `y ≺ x`. -/
+def symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
+
+/-- A relation is transitive if `x ≺ y` and `y ≺ z` together imply `x ≺ z`. -/
+def transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
+
+/-- An equivalance is a reflexive, symmetric, and transitive relation. -/
+def equivalence := reflexive r ∧ symmetric r ∧ transitive r
+
+/-- A relation is total if for all `x` and `y`, either `x ≺ y` or `y ≺ x`. -/
+def total := ∀ x y, x ≺ y ∨ y ≺ x
+
+lemma mk_equivalence (rfl : reflexive r) (symm : symmetric r) (trans : transitive r) :
+  equivalence r :=
+⟨rfl, symm, trans⟩
+
+/-- Irreflexive means "not reflexive". -/
+def irreflexive := ∀ x, ¬ x ≺ x
+
+/-- A relation is antisymmetric if `x ≺ y` and `y ≺ x` together imply that `x = y`. -/
+def anti_symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y
+
+/-- An empty relation does not relate any elements. -/
+@[nolint unusedArguments]
+def empty_relation := λ _ _ : α => False
+
+/-- `q` is a subrelation of `r` if for all `x` and `y`, `q x y` implies `r x y` -/
+def subrelation (q r : β → β → Prop) := ∀ ⦃x y⦄, q x y → r x y
+
+/-- Given `f : α → β`, a relation on `β` induces a relation on `α`.-/
+def inv_image (f : α → β) : α → α → Prop :=
+λ a₁ a₂ => f a₁ ≺ f a₂
+
+lemma inv_image.trans (f : α → β) (h : transitive r) : transitive (inv_image r f) :=
+λ (a₁ a₂ a₃ : α) (h₁ : inv_image r f a₁ a₂) (h₂ : inv_image r f a₂ a₃) => h h₁ h₂
+
+lemma inv_image.irreflexive (f : α → β) (h : irreflexive r) : irreflexive (inv_image r f) :=
+λ (a : α) (h₁ : inv_image r f a a) => h (f a) h₁
+
+end relation
 
 section binary
 variable {α : Type u} {β : Type v}