equal
deleted
inserted
replaced
9 text {* |
9 text {* |
10 Basic definition for equivalence relations |
10 Basic definition for equivalence relations |
11 that are represented by predicates. |
11 that are represented by predicates. |
12 *} |
12 *} |
13 |
13 |
14 (* TODO check where definitions can be changed to \<longleftrightarrow> *) |
|
15 definition |
14 definition |
16 "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))" |
15 "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))" |
17 |
16 |
18 definition |
17 definition |
19 "reflp E \<longleftrightarrow> (\<forall>x. E x x)" |
18 "reflp E \<longleftrightarrow> (\<forall>x. E x x)" |