equal
deleted
inserted
replaced
5 section \<open>Infinite Sets and Related Concepts\<close> |
5 section \<open>Infinite Sets and Related Concepts\<close> |
6 |
6 |
7 theory Infinite_Set |
7 theory Infinite_Set |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
|
10 |
|
11 lemma subset_image_inj: |
|
12 "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)" |
|
13 proof safe |
|
14 show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U" |
|
15 if "S \<subseteq> f ` T" |
|
16 proof - |
|
17 from that [unfolded subset_image_iff subset_iff] |
|
18 obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)" |
|
19 unfolding image_iff by metis |
|
20 show ?thesis |
|
21 proof (intro exI conjI) |
|
22 show "g ` S \<subseteq> T" |
|
23 by (simp add: g image_subsetI) |
|
24 show "inj_on f (g ` S)" |
|
25 using g by (auto simp: inj_on_def) |
|
26 show "S = f ` (g ` S)" |
|
27 using g image_subset_iff by auto |
|
28 qed |
|
29 qed |
|
30 qed blast |
10 |
31 |
11 subsection \<open>The set of natural numbers is infinite\<close> |
32 subsection \<open>The set of natural numbers is infinite\<close> |
12 |
33 |
13 lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)" |
34 lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)" |
14 for S :: "nat set" |
35 for S :: "nat set" |