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