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);