Miscellany.thy

   1 header {* Miscellaneous lemmas *}
   2 theory Miscellany
   3 imports Main
   4 begin
   5
   6 lemma bij_f_inv_f [simp]:
   7   assumes "bij f"
   8   shows "f (inv f x) = x"
   9   by (metis UNIV_I assms bij_betw_imp_surj f_inv_into_f)
  10
  11 lemma bij_f_x_equiv_inv_f_y [simp]:
  12   assumes "bij f"
  13   shows "inv f y = x \<longleftrightarrow> f x = y"
  14   by (metis assms bij_betw_def bij_f_inv_f inv_f_eq)
  15
  16 lemma bij_map_f_map_inv_f [simp]:
  17   assumes "bij f"
  18   shows "map f (map (inv f) xs) = xs"
  19   by (metis assms bij_betw_imp_surj list.map_id map_map surj_iff)
  20
  21 end