equal
deleted
inserted
replaced
8 |
8 |
9 theory Topology_Euclidean_Space |
9 theory Topology_Euclidean_Space |
10 imports |
10 imports |
11 Complex_Main |
11 Complex_Main |
12 "~~/src/HOL/Library/Countable_Set" |
12 "~~/src/HOL/Library/Countable_Set" |
13 "~~/src/HOL/Library/Glbs" |
|
14 "~~/src/HOL/Library/FuncSet" |
13 "~~/src/HOL/Library/FuncSet" |
15 Linear_Algebra |
14 Linear_Algebra |
16 Norm_Arith |
15 Norm_Arith |
17 begin |
16 begin |
18 |
17 |
25 using dist_triangle[of y z x] by (simp add: dist_commute) |
24 using dist_triangle[of y z x] by (simp add: dist_commute) |
26 |
25 |
27 (* LEGACY *) |
26 (* LEGACY *) |
28 lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l" |
27 lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l" |
29 by (rule LIMSEQ_subseq_LIMSEQ) |
28 by (rule LIMSEQ_subseq_LIMSEQ) |
30 |
|
31 lemmas real_isGlb_unique = isGlb_unique[where 'a=real] |
|
32 |
29 |
33 lemma countable_PiE: |
30 lemma countable_PiE: |
34 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |
31 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |
35 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
32 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
36 |
33 |
1553 assume a: "a < Inf (f ` ({x<..} \<inter> I))" |
1550 assume a: "a < Inf (f ` ({x<..} \<inter> I))" |
1554 { |
1551 { |
1555 fix y |
1552 fix y |
1556 assume "y \<in> {x<..} \<inter> I" |
1553 assume "y \<in> {x<..} \<inter> I" |
1557 with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y" |
1554 with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y" |
1558 by (auto intro: cInf_lower) |
1555 by (auto intro!: cInf_lower bdd_belowI2) |
1559 with a have "a < f y" |
1556 with a have "a < f y" |
1560 by (blast intro: less_le_trans) |
1557 by (blast intro: less_le_trans) |
1561 } |
1558 } |
1562 then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))" |
1559 then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))" |
1563 by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one) |
1560 by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one) |