equal
deleted
inserted
replaced
488 assumes T2: "\<And>P. (\<And>x. P x) \<Longrightarrow> (\<And>x. T P x)" |
488 assumes T2: "\<And>P. (\<And>x. P x) \<Longrightarrow> (\<And>x. T P x)" |
489 assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x" |
489 assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x" |
490 shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x" |
490 shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x" |
491 proof - |
491 proof - |
492 from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x" |
492 from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x" |
493 unfolding eventually_INF[of _ I] by auto |
493 unfolding eventually_INF[of _ _ I] by auto |
494 moreover then have "eventually (T P) (INFIMUM X F')" |
494 moreover then have "eventually (T P) (INFIMUM X F')" |
495 apply (induction X arbitrary: P) |
495 apply (induction X arbitrary: P) |
496 apply (auto simp: eventually_inf T2) |
496 apply (auto simp: eventually_inf T2) |
497 subgoal for x S P Q R |
497 subgoal for x S P Q R |
498 apply (intro exI[of _ "T Q"]) |
498 apply (intro exI[of _ "T Q"]) |