equal
deleted
inserted
replaced
1 (* Title: HOL/ZF/Helper.thy |
|
2 ID: $Id$ |
|
3 Author: Steven Obua |
|
4 |
|
5 Some helpful lemmas that probably will end up elsewhere. |
|
6 *) |
|
7 |
|
8 theory Helper |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)" |
|
13 apply auto |
|
14 apply (subgoal_tac "P (THE x. P x)") |
|
15 apply blast |
|
16 apply (rule theI) |
|
17 apply auto |
|
18 done |
|
19 |
|
20 lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)" |
|
21 by auto |
|
22 |
|
23 lemma f_x_in_range_f: "f x \<in> range f" |
|
24 by (blast intro: image_eqI) |
|
25 |
|
26 lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)" |
|
27 by (blast intro: comp_inj_on subset_inj_on) |
|
28 |
|
29 lemma comp_image_eq: "(g o f) ` x = g ` f ` x" |
|
30 by auto |
|
31 |
|
32 end |
|