--- a/src/HOL/BNF_Least_Fixpoint.thy Sun Aug 09 12:51:54 2020 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy Sun Aug 09 13:18:40 2020 +0100
@@ -37,13 +37,6 @@
lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
unfolding underS_def Field_def by auto
-lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
- unfolding bij_betw_def by auto
-
-lemma f_the_inv_into_f_bij_betw:
- "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
- unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
-
lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
by (subst (asm) internalize_card_of_ordLeq) (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])