equal
deleted
inserted
replaced
373 
373 
374 (*NOT suitable for rewriting*) 
374 (*NOT suitable for rewriting*) 
375 Goal "r^^B = (UN y: B. r^^{y})"; 
375 Goal "r^^B = (UN y: B. r^^{y})"; 
376 by (Blast_tac 1); 
376 by (Blast_tac 1); 
377 qed "Image_eq_UN"; 
377 qed "Image_eq_UN"; 

378 

379 Goal "[ r'<=r; A'<=A ] ==> (r' ^^ A') <= (r ^^ A)"; 

380 by (Blast_tac 1); 

381 qed "Image_mono"; 

382 

383 Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))"; 

384 by (Blast_tac 1); 

385 qed "Image_UN"; 

386 

387 (*Converse inclusion fails*) 

388 Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))"; 

389 by (Blast_tac 1); 

390 qed "Image_INT_subset"; 
378 
391 
379 
392 
380 section "Univalent"; 
393 section "Univalent"; 
381 
394 
382 Goalw [Univalent_def] 
395 Goalw [Univalent_def] 