Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Fun.ML
changeset 7051 9b6bdced3dc6
parent 7014 11ee650edcd2
child 7089 9bfb8e218b99
equal deleted inserted replaced
7050:c70d3402fef5 7051:9b6bdced3dc6 
   172 qed "surjD";
 
   172 qed "surjD";
 
   173 
   173 
   174 
   174 
   175 (*** Lemmas about injective functions and inv ***)
 
   175 (*** Lemmas about injective functions and inv ***)
 
   176 
   176 
   177 Goalw [o_def] "[| inj_on f A;  inj_on g (range f) |] ==> inj_on (g o f) A";
 
   177 Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
 
   178 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
 
   178 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
 
   179 qed "comp_inj_on";
 
   179 qed "comp_inj_on";
 
   180 
   180 
   181 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
 
   181 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
 
   182 by (fast_tac (claset() addIs [selectI]) 1);
 
   182 by (fast_tac (claset() addIs [selectI]) 1);
isabelle