equal
deleted
inserted
replaced
39 |
39 |
40 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
40 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
41 unfolding Field_def by auto |
41 unfolding Field_def by auto |
42 |
42 |
43 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B" |
43 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B" |
44 unfolding bij_betw_def by auto |
|
45 |
|
46 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B" |
|
47 unfolding bij_betw_def by auto |
44 unfolding bij_betw_def by auto |
48 |
45 |
49 lemma f_the_inv_into_f_bij_betw: |
46 lemma f_the_inv_into_f_bij_betw: |
50 "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x" |
47 "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x" |
51 unfolding bij_betw_def by (blast intro: f_the_inv_into_f) |
48 unfolding bij_betw_def by (blast intro: f_the_inv_into_f) |