equal
deleted
inserted
replaced
123 lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)" |
123 lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)" |
124 unfolding Bfun_def eventually_sequentially |
124 unfolding Bfun_def eventually_sequentially |
125 proof safe |
125 proof safe |
126 fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K" |
126 fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K" |
127 then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" |
127 then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" |
128 by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2) |
128 by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) |
129 (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) |
129 (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) |
130 qed auto |
130 qed auto |
131 |
131 |
132 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
132 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
133 unfolding Bseq_def by auto |
133 unfolding Bseq_def by auto |