Right at the end of the file `init/logic.lean`

in core lean, there are definitions of the basic relations on types such as `reflexive`

, `irreflexive`

, `symmetric`

, `anti_symmetric`

, `transitive`

, `equivalence`

, and `total`

(i.e. for all `x`

and `y`

, `x R y`

or `y R x`

). One key usage of equivalence relations is the construction of equivalence classes; this is well documented in Theorem Proving In Lean.

## Examples.

```
variable (X : Type*)
-- equality is symmetric
example : symmetric (λ x y : X, x=y) := λ x y, eq.symm
-- "less than" is transitive on the natural numbers.
example : transitive (λ a b : nat, a<b) := λ x y z : nat, lt_trans
```

Advertisements