[STATEMENT]
lemma sets_Collect_Cauchy[measurable]:
  fixes f :: "nat \<Rightarrow> 'a => 'b::{metric_space, second_countable_topology}"
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
  shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. Cauchy (\<lambda>i. f i x)} \<in> sets M
[PROOF STEP]
unfolding metric_Cauchy_iff2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. \<forall>j. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < inverse (real (Suc j))} \<in> sets M
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f ?i \<in> borel_measurable M

goal (1 subgoal):
 1. {x \<in> space M. \<forall>j. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < inverse (real (Suc j))} \<in> sets M
[PROOF STEP]
by auto