src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 56166 9a241bc276cd
parent 56154 f0a927235162
child 56188 0268784f60da
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -1548,7 +1548,7 @@
     1.4        fix y
     1.5        assume "y \<in> {x<..} \<inter> I"
     1.6        with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
     1.7 -        by (auto intro!: cInf_lower bdd_belowI2)
     1.8 +        by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq)
     1.9        with a have "a < f y"
    1.10          by (blast intro: less_le_trans)
    1.11      }
    1.12 @@ -3116,7 +3116,7 @@
    1.13      fix X
    1.14      assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
    1.15      then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
    1.16 -      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD)
    1.17 +      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
    1.18      with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
    1.19        by auto
    1.20      with B show False