equal
deleted
inserted
replaced
345 and predicates. Added powers of predicate relations. Consolidation |
345 and predicates. Added powers of predicate relations. Consolidation |
346 of some relation theorems: |
346 of some relation theorems: |
347 |
347 |
348 converse_def ~> converse_unfold |
348 converse_def ~> converse_unfold |
349 rel_comp_def ~> relcomp_unfold |
349 rel_comp_def ~> relcomp_unfold |
350 symp_def ~> (dropped, use symp_def and sym_def instead) |
350 symp_def ~> (modified, use symp_def and sym_def instead) |
351 transp_def ~> transp_trans |
351 transp_def ~> transp_trans |
352 Domain_def ~> Domain_unfold |
352 Domain_def ~> Domain_unfold |
353 Range_def ~> Domain_converse [symmetric] |
353 Range_def ~> Domain_converse [symmetric] |
354 |
354 |
355 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. |
355 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. |