src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Fri Feb 21 17:51:56 2020 +0100
+++ b/src/HOL/Fun.thy	Mon Feb 24 12:14:13 2020 +0000
@@ -341,6 +341,9 @@
 lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   unfolding bij_betw_def by simp
 
+lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
+  unfolding bij_betw_def by auto
+
 lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
   by (rule bij_betw_def)