src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 58757 7f4924f23158
parent 58184 db1381d811ab
child 58759 e55fe82f3803
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 21 21:20:45 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 21 21:32:12 2014 +0200
     1.3 @@ -1015,7 +1015,7 @@
     1.4      and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> cbox a b"
     1.5       and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
     1.6    unfolding subset_eq[unfolded Ball_def] unfolding mem_box
     1.7 -   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
     1.8 +  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
     1.9  
    1.10  lemma box_subset_cbox:
    1.11    fixes a :: "'a::euclidean_space"
    1.12 @@ -1153,7 +1153,9 @@
    1.13  
    1.14  lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
    1.15  proof -
    1.16 -  { fix x b :: 'a assume [simp]: "b \<in> Basis"
    1.17 +  {
    1.18 +    fix x b :: 'a
    1.19 +    assume [simp]: "b \<in> Basis"
    1.20      have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)"
    1.21        by (rule real_natceiling_ge)
    1.22      also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    1.23 @@ -1679,7 +1681,7 @@
    1.24    by (simp add: frontier_def)
    1.25  
    1.26  lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
    1.27 -proof-
    1.28 +proof -
    1.29    {
    1.30      assume "frontier S \<subseteq> S"
    1.31      then have "closure S \<subseteq> S"
    1.32 @@ -1690,13 +1692,14 @@
    1.33    then show ?thesis using frontier_subset_closed[of S] ..
    1.34  qed
    1.35  
    1.36 -lemma frontier_complement: "frontier(- S) = frontier S"
    1.37 +lemma frontier_complement: "frontier (- S) = frontier S"
    1.38    by (auto simp add: frontier_def closure_complement interior_complement)
    1.39  
    1.40  lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
    1.41    using frontier_complement frontier_subset_eq[of "- S"]
    1.42    unfolding open_closed by auto
    1.43  
    1.44 +
    1.45  subsection {* Filters and the ``eventually true'' quantifier *}
    1.46  
    1.47  definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"