Rel.v
Table of Contents
- 1. Summary
- 2. Notes
- 3. Exercises
- 4. Scores
- 5. Questions
- 6. Metacognition
- 7. Further Knowledge
- 7.1. Setoids
- 7.2. Quotient set
- 7.3. Lower/upper set
- 7.4. Dedekind cut
- 7.5. Fence
- 7.6. Lexicographic order
- 7.7. Product order
- 7.8. Direct product
- 7.9. Chain
- 7.10. Antichain
- 7.11. Maximal/minimal element
- 7.12. Greatest/lowest element
- 7.13. Order-preserving function
- 7.14. Order-reflecting function
- 7.15. Zorn’s lemma
- 8. TODOs
Homepage | Previous: Maps.v | Code | Next: Wrapping up
1. Summary
A relation is a proposition about pairs of elements. The notions of partial and total functions were introduced as well as reflexivity, transitivity, symmetry and antisymmetry. The exercises were useful for practicing induction on propositions. Types of transitive relations were discussed - equivalence relations, preorders, partial orders. Finally, two definitions of reflexive and transitive closures were introduced and were shown to be equivalent.
1.1. Terms
relation, partial, total, reflexivity, transitivity, symmetry, antisymmetry, equivalence relation, preorder, partial order, closure, reflexive transitive closure.
2. Notes
N/A
3. Exercises
The Search tactic was helpful. Some of the later exercises were annoying in that there were too many things to induct on - one needs to pay attention to the inductive propositions - it is good to draw them via proof trees.
3.1. total_relation_not_partial_function
2 stars, standard, optional
The total_relation function doesn’t seem to exist in IndProp.v.
3.2. empty_relation_partial_function
2 stars, standard, optional
The empty_relation function doesn’t seem to exist in IndProp.v.
3.3. le_trans_hard_way
2 stars, standard, optional
3.4. lt_trans''
2 stars, standard, optional
3.5. le_S_n
1 star, standard, optional
3.6. le_Sn_n_inf
2 stars, standard, optional
3.7. le_Sn_n
1 star, standard, optional
3.8. le_not_symmetric
2 stars, standard, optional
3.9. le_antisymmetric
2 stars, standard, optional
3.10. le_step
2 stars, standard, optional
3.11. rsc_trans
2 stars, standard, optional
3.12. rtc_rsc_coincide
3 stars, standard, optional
4. Scores
5. Questions
6. Metacognition
The chapter was short and the exercises were the most important part of this.
7. Further Knowledge
Some very random notes on order theory / algebra.
7.1. Setoids
A setoid is a set X with an equivalence relation ~. A setoid distinguishes intensional equality and extensional equality (equivalence). Intenional equality is equality on X, while extensional equality is equality on the quotient set X/~.
7.2. Quotient set
The quotient set of X given a equivalence relation R is denoted X/R or X modulo R. It is set of all equivalence classes in X with respect to R.
7.3. Lower/upper set
A subset that is upward or downward closed in a poset/proset.
7.4. Dedekind cut
Generalized, it is a parition of a totally ordered set X into (L, U) where L is downwards closed, inhabited, and has no largest element; while U is upwards closed.
7.5. Fence
Also called a zigzag poset. It is a poset with elements a, b, c, d, ... such that a < b > c < d ...
7.6. Lexicographic order
A relation \leq on a cartesian product X x Y such that (a, b) \leq (c,d) if a < b or (a = c and b \leq d), where a, c \in X, b, d \in Y.
7.7. Product order
A relation \leq on a cartesian product X x Y such that (a, b) \leq (c,d) if a \leq c or a \leq d.
7.8. Direct product
Thought of as inducing a structure on the cartesian product of the sets of the contributing objects.
7.9. Chain
A totally ordered set of a poset.
7.10. Antichain
A subset of a poset where no distinct pair is comparable.
7.11. Maximal/minimal element
For poset P, a g \in P such that ~\exists a \in P. a > g (maximal) or ~\exists a \in P. a > g (minimal)
7.12. Greatest/lowest element
The unique maximal or minimal element of a poset P.
7.13. Order-preserving function
Also called monotone function. A function f from A to B where \forall x, y \ in A, if x \leq y then f(x) \leq f(y).
7.14. Order-reflecting function
A function f from A to B where \forall x, y \ in A, if f(x) \leq f(y) then x \leq y.
7.15. Zorn’s lemma
States that a poset with upper bounds for all chains has at least one maximal element.