src/HOL/Library/FuncSet.thy
changeset 63060 293ede07b775
parent 62390 842917225d56
child 63092 a949b2a5f51d
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:39:17 2016 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:44:31 2016 +0200
     1.3 @@ -96,9 +96,9 @@
     1.4    assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
     1.5    then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
     1.6      by auto
     1.7 -  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
     1.8 +  from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
     1.9      by auto
    1.10 -  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
    1.11 +  obtain k where k: "n i \<le> k" if "i \<in> I" for i
    1.12      using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
    1.13    have "f \<in> Pi I (A k)"
    1.14    proof (intro Pi_I)