equal
deleted
inserted
replaced
266 shows "(x = y) = R (Rep x) (Rep y)" |
266 shows "(x = y) = R (Rep x) (Rep y)" |
267 by (rule QUOTIENT_REL_REP[OF q, symmetric]) |
267 by (rule QUOTIENT_REL_REP[OF q, symmetric]) |
268 |
268 |
269 lemma EQUALS_RSP: |
269 lemma EQUALS_RSP: |
270 assumes q: "QUOTIENT R Abs Rep" |
270 assumes q: "QUOTIENT R Abs Rep" |
271 and a: "R x1 x2" "R y1 y2" |
271 and a: "R xa xb" "R ya yb" |
272 shows "R x1 y1 = R x2 y2" |
272 shows "R xa ya = R xb yb" |
273 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def |
273 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def |
274 using a by blast |
274 using a by blast |
275 |
275 |
276 lemma LAMBDA_PRS: |
276 lemma LAMBDA_PRS: |
277 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
277 assumes q1: "QUOTIENT R1 Abs1 Rep1" |