85 assume "\<exists>i. x \<in> A i" |
85 assume "\<exists>i. x \<in> A i" |
86 then obtain i where "x \<in> A i" |
86 then obtain i where "x \<in> A i" |
87 by auto |
87 by auto |
88 then have |
88 then have |
89 "\<And>n. (indicator (A (n + i)) x :: 'a) = 1" |
89 "\<And>n. (indicator (A (n + i)) x :: 'a) = 1" |
90 "(indicator (\<Union> i. A i) x :: 'a) = 1" |
90 "(indicator (\<Union>i. A i) x :: 'a) = 1" |
91 using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def) |
91 using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def) |
92 then show ?thesis |
92 then show ?thesis |
93 by (rule_tac LIMSEQ_offset[of _ i]) simp |
93 by (rule_tac LIMSEQ_offset[of _ i]) simp |
94 qed (auto simp: indicator_def) |
94 qed (auto simp: indicator_def) |
95 |
95 |
96 lemma LIMSEQ_indicator_UN: |
96 lemma LIMSEQ_indicator_UN: |
97 "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x" |
97 "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x" |
98 proof - |
98 proof - |
99 have "(\<lambda>k. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x" |
99 have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x" |
100 by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans) |
100 by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans) |
101 also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. A i)" |
101 also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)" |
102 by auto |
102 by auto |
103 finally show ?thesis . |
103 finally show ?thesis . |
104 qed |
104 qed |
105 |
105 |
106 lemma LIMSEQ_indicator_decseq: |
106 lemma LIMSEQ_indicator_decseq: |
121 lemma LIMSEQ_indicator_INT: |
121 lemma LIMSEQ_indicator_INT: |
122 "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x" |
122 "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x" |
123 proof - |
123 proof - |
124 have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x" |
124 have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x" |
125 by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans) |
125 by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans) |
126 also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. A i)" |
126 also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)" |
127 by auto |
127 by auto |
128 finally show ?thesis . |
128 finally show ?thesis . |
129 qed |
129 qed |
130 |
130 |
131 lemma indicator_add: |
131 lemma indicator_add: |