src/HOL/BNF_Least_Fixpoint.thy
changeset 58159 e3d1912a0c8f
parent 58147 967444d352b8
child 58179 2de7b0313de3
equal deleted inserted replaced
58158:d2cb7cbb3aaa 58159:e3d1912a0c8f
    64   unfolding bij_betw_def by auto
    64   unfolding bij_betw_def by auto
    65 
    65 
    66 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
    66 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
    67   unfolding bij_betw_def by auto
    67   unfolding bij_betw_def by auto
    68 
    68 
    69 lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
    69 lemma f_the_inv_into_f_bij_betw:
    70   (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    70   "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    71   unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
    71   unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
    72 
    72 
    73 lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
    73 lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
    74   by (subst (asm) internalize_card_of_ordLeq)
    74   by (subst (asm) internalize_card_of_ordLeq) (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
    75     (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
       
    76 
    75 
    77 lemma bij_betwI':
    76 lemma bij_betwI':
    78   "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
    77   "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
    79     \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
    78     \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
    80     \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
    79     \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"